EntryExpr

Mathlib.Tactic.CC.Datatypes

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

Lean4

/-- This is used as a proof term in `Entry`s instead of `Expr`. -/
inductive EntryExpr/-- An `EntryExpr` of just an `Expr`. -/

  | ofExpr (e : Expr) : EntryExpr/-- dummy congruence proof, it is just a placeholder. -/

  | congr : EntryExpr/-- dummy eq_true proof, it is just a placeholder -/

  | eqTrue : EntryExpr/-- dummy refl proof, it is just a placeholder. -/

  | refl : EntryExpr/-- An `EntryExpr` of a `DelayedExpr`. -/

  | ofDExpr (e : DelayedExpr) : EntryExpr
  deriving Inhabited

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

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

Разделы

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

Аффилиация

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