ppEqc

Mathlib.Tactic.CC.Datatypes

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

Lean4

/-- Pretty print the entry associated with the given expression. -/
def ppEqc (ccs : CCState) (e : Expr) : MessageData :=
  Id.run
    (do
      let mut lr : List MessageData := []
      let mut it := e
      repeat
        let some itN := ccs.entries[it]? |
          break
        let mdIt : MessageData := if it.isForall || it.isLambda || it.isLet then paren (ofExpr it) else ofExpr it
        lr := mdIt :: lr
        it := itN.next
      until it == e
      let l := lr.reverse
      return bracket "{" (group <| joinSep l (ofFormat ("," ++ .line))) "}")

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

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

Разделы

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

Аффилиация

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