removeCHoles

Mathlib.Tactic.TermCongr

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.TermCongr.removeCHoles

Lean4

/-- Eliminate all congruence holes from an expression by replacing them with their values. -/
def removeCHoles (e : Expr) : Expr :=
  e.replace fun e' => if let some (_, val, _) := cHole? e' then val else none

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru