Pi type notation #
Π 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
open scoped PiNotation.
The notation also accepts extended binders, like
Π x ∈ s, β x for
Π x, x ∈ s → β x.
Since pi notation and forall notation are interchangeable, we can parse it by simply using the pre-existing forall parser.
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.
- One or more equations did not get rendered due to their size.