instToMessageDataEntryExpr

Mathlib.Tactic.CC.Datatypes

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

Lean4

instance : ToMessageData EntryExpr where
  toMessageData
    | .ofExpr e => toMessageData e
    | .congr => m!"[congruence proof]"
    | .eqTrue => m!"[eq_true proof]"
    | .refl => m!"[refl proof]"
    | .ofDExpr _ => m!"[delayed expression]"

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

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

Разделы

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

Аффилиация

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