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
.
This can be disabled with the pp.mathlib.binderPredicates
option.
Dependent function type (a "pi type"). The notation Π x : α, β x
can
also be written as (x : α) → β x
.
Equations
Instances For
Dependent function type (a "pi type"). The notation Π x ∈ s, β x
is
short for Π x, x ∈ s → β x
.
Equations
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
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
Instances For
Delaborator for existential quantifier, including extended binders.
Equations
Instances For
Delaborator for ∉
.