# Documentation

Lean.Elab.Syntax

Expand optional «precedence» where «precedence» := leading_parser " : " >> precedenceParser

Equations
Instances For
@[inline]
Equations
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.

(Try to) add a term info for the category catName at ref.

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

(Try to) add a term info for the alias with info info at ref.

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.
Equations
• One or more equations did not get rendered due to their size.

Given a stx of category syntax, return a (newStx, lhsPrec?), where newStx is of category term. After elaboration, newStx should have type TrailingParserDescr if lhsPrec?.isSome, and ParserDescr otherwise.

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

Sequence (aka NullNode)

Equations
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.
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.

Auxiliary function for creating declaration names from parser descriptions. Example: Given

syntax term "+" term : term
syntax "[" sepBy(term, ", ") "]"  : term


It generates the names term_+_ and term[_,]

Equations
• One or more equations did not get rendered due to their size.
Equations
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.
def Lean.Elab.Command.addMacroScopeIfLocal {m : } [inst : ] [inst : ] (name : Lean.Name) (attrKind : Lean.Syntax) :

Add macro scope to name if it does not already have them, and attrKind is local.

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.
Equations
def Lean.Elab.Command.inferMacroRulesAltKind :
Lean.TSyntax Lean.Parser.Term.matchAlt
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.Command.expandNoKindMacroRulesAux (alts : Array (Lean.TSyntax Lean.Parser.Term.matchAlt)) (cmdName : String) (mkCmd : Array (Lean.TSyntax Lean.Parser.Term.matchAlt)) :

Infer syntax kind k from first pattern, put alternatives of same kind into new macro/elab_rules (kind := k) via mkCmd (some k), leave remaining alternatives (via mkCmd none`) to be recursively expanded.

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