delabWithUniv

Mathlib.Tactic.PPWithUniv

URI: https://scilib.ai/kg/mathlib#Mathlib.PPWithUniv.delabWithUniv

Lean4

/-- Delaborator that prints the current application with universe parameters on the head symbol,
unless `pp.universes` is explicitly set to `false`.
-/
def delabWithUniv : Delab :=
  whenPPOption (·.get pp.universes.name true) <|
    let enablePPUnivOnHead subExpr :=
      let expr := subExpr.expr
      let expr := mkAppN (expr.getAppFn.setOption pp.universes.name true) expr.getAppArgs
      { subExpr with expr }
    withTheReader SubExpr enablePPUnivOnHead delabApp

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

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

Разделы

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

Аффилиация

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