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

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.
Instances For

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.
Instances For

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

Equations
Instances For

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.
Instances For

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.
Instances For

Delaborator for existential quantifier, including extended binders.

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

Delaborator for ∉.

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