# 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

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

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