isEqTrue

Mathlib.Tactic.CC.MkProof

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCM.isEqTrue

Lean4

/-- Is the proposition `e` known to be true? -/
@[inline]
def isEqTrue (e : Expr) : CCM Bool :=
  isEqv e (.const ``True [])

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

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

Разделы

Аффилиация

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