mkDefault'

Mathlib.Tactic.TermCongr

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.TermCongr.CongrResult.mkDefault'

Lean4

/-- Does `CongrResult.mkDefault` but makes sure there are no lingering congruence holes. -/
def mkDefault' (mvarCounterSaved : Nat) (lhs rhs : Expr) : MetaM CongrResult := do
  if let some h := hasCHole mvarCounterSaved lhs then
    throwError "Left-hand side{(indentD lhs)}\nstill has a congruence hole{indentD h}"
  if let some h := hasCHole mvarCounterSaved rhs then
    throwError "Right-hand side{(indentD rhs)}\nstill has a congruence hole{indentD h}"
  CongrResult.mkDefault lhs rhs

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

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

Разделы

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

Аффилиация

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