Documentation

Mathlib.Mathport.Notation

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.