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

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.

Instances For

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.

Instances For

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

- PiNotation.replacePiNotation (Lean.Syntax.node info kind args) = pure (Lean.Syntax.node info `Lean.Parser.Term.forall args)
- PiNotation.replacePiNotation x✝ = Lean.Macro.throwUnsupported

Instances For

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.

Instances For

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.

Instances For

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.

Instances For

source
def delab_not_in :
Lean.PrettyPrinter.Delaborator.Delab

Delaborator for `∉`.

Equations

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

Instances For