The notation3 macro, simulating Lean 3's notation. #
Expands binders into nested combinators.
For example, the familiar exists is given by:
expand_binders% (p => Exists p) x y : Nat, x < y
which expands to the same expression as
∃ x y : Nat, x < y
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Keywording indicating whether to use a left- or right-fold.
Equations
- One or more equations did not get rendered due to their size.
notation3
argument matching extBinders
.
Equations
- One or more equations did not get rendered due to their size.
notation3
argument simulating a Lean 3 fold notation.
Equations
- One or more equations did not get rendered due to their size.
notation3
argument binding a name.
Equations
- One or more equations did not get rendered due to their size.
notation3
argument.
Equations
- One or more equations did not get rendered due to their size.
notation3
declares notation using Lean 3-style syntax. This command can be used in mathlib4
but it has an uncertain future and exists primarily for backward compatibility.
Equations
- One or more equations did not get rendered due to their size.