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

                          Equations
                            Instances For