heq

Mathlib.Tactic.TermCongr

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

Lean4

/-- Returns the proof that `lhs ≍ rhs`. Fails if the `CongrResult` is inapplicable.
If `pf? = none`, this returns the `rfl` proof. -/
def heq (res : CongrResult) : MetaM Expr := do
  match res.pf? with
  | some pf =>
    pf .heq
  | none =>
    mkHEqRefl res.lhs

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

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

Разделы

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

Аффилиация

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