Documentation

Mathlib.Util.Delaborators

Pi type notation #

Provides the Π x : α, β x notation as an alternative to Lean 4's built-in (x : α) → β x notation. To get all non-∀ pi types to pretty print this way then do open scoped PiNotation.

The notation also accepts extended binders, like Π x ∈ s, β x for Π x, x ∈ s → β x.

source
def PiNotation.piNotation :
Lean.Parser.Parser

Dependent function type (a "pi type"). The notation Π x : α, β x can also be written as (x : α) → β x.

Equations
  • One or more equations did not get rendered due to their size.
source
def PiNotation.«termΠ__,_» :
Lean.ParserDescr

Dependent function type (a "pi type"). The notation Π x ∈ s, β x is short for Π x, x ∈ s → β x.

Equations
  • One or more equations did not get rendered due to their size.
source
def PiNotation.replacePiNotation :
Lean.Macro

Since pi notation and forall notation are interchangeable, we can parse it by simply using the pre-existing forall parser.

Equations
source
def PiNotation.delabPi :
Lean.PrettyPrinter.Delaborator.Delab

Override the Lean 4 pi notation delaborator with one that prints cute binders such as ∀ ε > 0.

Equations
  • One or more equations did not get rendered due to their size.
source
def PiNotation.delabPi' :
Lean.PrettyPrinter.Delaborator.Delab

Override the Lean 4 pi notation delaborator with one that uses Π and prints cute binders such as ∀ ε > 0. Note that this takes advantage of the fact that (x : α) → p x notation is never used for propositions, so we can match on this result and rewrite it.

Equations
  • One or more equations did not get rendered due to their size.
source
def exists_delab :
Lean.PrettyPrinter.Delaborator.Delab

Delaborator for existential quantifier, including extended binders.

Equations
  • One or more equations did not get rendered due to their size.
source
def delab_not_in :
Lean.PrettyPrinter.Delaborator.Delab

Delaborator for ∉.

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