isRfl

Mathlib.Tactic.TermCongr

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

Lean4

/-- Returns whether the proof is by reflexivity.
Such congruence proofs are trivial. -/
def isRfl (res : CongrResult) : Bool :=
  res.pf?.isNone

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

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

Разделы

Аффилиация

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