The notation3 macro, simulating Lean 3's notation.

ink

def Lean.Parser.Command.«termExpand_binders%(_=>_)_,_» : Lean.ParserDescr

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.

ink

def Lean.Parser.Command.expandFoldl : Lean.ParserDescr

Equations

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

ink

def Lean.Parser.Command.expandFoldr : Lean.ParserDescr

Equations

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

ink

def Lean.Parser.Command.foldKind : Lean.ParserDescr

Keywording indicating whether to use a left- or right-fold.

Equations

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

ink

def Lean.Parser.Command.bindersItem : Lean.ParserDescr

notation3 argument matching extBinders.

Equations

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

ink

def Lean.Parser.Command.foldAction : Lean.ParserDescr

notation3 argument simulating a Lean 3 fold notation.

Equations

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

ink

def Lean.Parser.Command.identOptScoped : Lean.ParserDescr

notation3 argument binding a name.

Equations

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

ink

def Lean.Parser.Command.notation3Item : Lean.ParserDescr

notation3 argument.

Equations

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

ink

def Lean.Parser.Command.«command___Notation3____=>_» : Lean.ParserDescr

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.