Documentation

Lean.Elab.Notation

source
def Lean.Elab.Command.addInheritDocDefault (rhs : Lean.Term) (attrs? : Option (Lean.Syntax.TSepArray (Lean.Name.mkStr4 "Lean" "Parser" "Term" "attrInstance") ",")) :
Option (Lean.Syntax.TSepArray (Lean.Name.mkStr4 "Lean" "Parser" "Term" "attrInstance") ",")
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.expandNotationItemIntoSyntaxItem :
Lean.TSyntax (Lean.Name.mkStr4 "Lean" "Parser" "Command" "notationItem") → Lean.MacroM (Lean.TSyntax (Lean.Name.mkStr1 "stx"))

Convert notation command lhs item into a syntax command item

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

Convert notation command lhs item into a pattern element

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.Name.mkStr4 "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.