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.

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).