Attribute to pretty-print universe level parameters by default

This module contains the pp_with_univ attribute, which enables pretty-printing of universe parameters for the associated declaration. This is helpful for definitions like Ordinal, where the universe levels are both relevant and not deducible from the arguments.

def Mathlib.PPWithUniv.delabWithUniv : Lean.PrettyPrinter.Delaborator.Delab

Delaborator that prints the current application with universe parameters on the head symbol, unless pp.universes is explicitly set to false.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.PPWithUniv.ppWithUnivAttr : Lean.ParserDescr

attribute [pp_with_univ] Ordinal instructs the pretty-printer to print Ordinal.{u} with universe parameters by default (unless pp.universes is explicitly set to false).

Equations

• Mathlib.PPWithUniv.ppWithUnivAttr = Lean.ParserDescr.node `Mathlib.PPWithUniv.ppWithUnivAttr 1024 (Lean.ParserDescr.nonReservedSymbol "pp_with_univ" false)