proofFor

Mathlib.Tactic.CC

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCState.proofFor

Lean4

/-- `proofFor cc e` constructs a proof for e if it is equivalent to true in `CCState` -/
def proofFor (ccs : CCState) (e : Expr) : MetaM Expr := do
  let (some r, _) ← CCM.run (CCM.getEqProof e (.const ``True [])) { ccs with } |
    throwError"CCState.proofFor failed to build proof"
  mkAppM ``of_eq_true #[r]

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

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

Разделы

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

Аффилиация

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