Documentation

Lean.Elab.Notation

source
def Lean.Elab.Command.expandNotationItemIntoSyntaxItem:
Lean.TSyntax `Lean.Parser.Command.notationItem → Lean.MacroM (Lean.TSyntax `stx)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.expandNotationItemIntoPattern (stx : Lean.Syntax) :
Lean.MacroM Lean.Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.removeParenthesesAux (parens : Lean.Syntax) (body : Lean.Syntax) :
Lean.Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Command.removeParentheses (stx : Lean.Syntax) :
Lean.MacroM Lean.Syntax
source
def Lean.Elab.Command.hasDuplicateAntiquot (stxs : Array Lean.Syntax) :
Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.mkSimpleDelab (attrKind : Lean.TSyntax `Lean.Parser.Term.attrKind) (pat : Lean.Term) (qrhs : Lean.Term) :
OptionT Lean.MacroM Lean.Syntax

Try to derive a SimpleDelab from a notation. The notation must be of the form notation ... => c body where c is a declaration in the current scope and body any syntax that contains each variable from the LHS at most once.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.expandNotation:
Lean.Macro
Equations
  • One or more equations did not get rendered due to their size.