Documentation

Mathlib.Tactic.PPWithUniv

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.

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

Instances For

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

    Instances For