def Lean.Elab.Term.expandOptPrecedence (stx : Syntax) : MacroM (Option Nat)

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

structure Lean.Elab.Term.ToParserDescrContext : Type

• catName : Name
• first : Bool
• leftRec : Bool
• behavior : Parser.LeadingIdentBehavior

  See comment at Parser.ParserCategory.

@[reducible, inline]

abbrev Lean.Elab.Term.ToParserDescrM (α : Type) : Type

@[reducible, inline]

abbrev Lean.Elab.Term.ToParserDescr : Type

def Lean.Elab.Term.ensureUnaryOutput (x : Term × Nat) : Term

def Lean.Elab.Term.addCategoryInfo (ref : Syntax) (catName : Name) : TermElabM Unit

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

def Lean.Elab.Term.addAliasInfo (ref : Syntax) (info : Parser.ParserAliasInfo) : TermElabM Unit

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

def Lean.Elab.Term.checkLeftRec (stx : Syntax) : ToParserDescrM Bool

def Lean.Elab.Term.elabParserName? (stx : Ident) : TermElabM (Option Parser.ParserResolution)

def Lean.Elab.Term.elabParserName (stx : Ident) : TermElabM Parser.ParserResolution

def Lean.Elab.Term.toParserDescr (stx : Syntax) (catName : Name) : TermElabM (Term × Option Nat)

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.

partial def Lean.Elab.Term.toParserDescr.process (stx : Syntax) : ToParserDescr

partial def Lean.Elab.Term.toParserDescr.processSeq (stx : Syntax) : ToParserDescrM (Term × Nat)

Sequence (aka NullNode)

def Lean.Elab.Term.toParserDescr.ensureNoPrec (stx : Syntax) : ToParserDescrM PUnit

def Lean.Elab.Term.toParserDescr.processParserCategory (stx : Syntax) : ToParserDescrM (Term × Nat)

partial def Lean.Elab.Term.toParserDescr.processAlias (id : Syntax) (args : Array Syntax) : ToParserDescrM (Term × Nat)

partial def Lean.Elab.Term.toParserDescr.processNullaryOrCat (stx : Syntax) : ToParserDescrM (Term × Nat)

partial def Lean.Elab.Term.toParserDescr.processSepBy (stx : Syntax) : ToParserDescrM (Term × Nat)

partial def Lean.Elab.Term.toParserDescr.processSepBy1 (stx : Syntax) : ToParserDescrM (Term × Nat)

def Lean.Elab.Term.toParserDescr.isValidAtom (s : String) : Bool

def Lean.Elab.Term.toParserDescr.processAtom (stx : Syntax) : ToParserDescrM (Term × Nat)

def Lean.Elab.Term.toParserDescr.processNonReserved (stx : Syntax) : ToParserDescrM (Term × Nat)

def Lean.Elab.Command.elabDeclareSyntaxCat : CommandElab

def Lean.Elab.Command.mkNameFromParserSyntax (catName : Name) (stx : Syntax) : MacroM Name

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[_,]

partial def Lean.Elab.Command.mkNameFromParserSyntax.visit (stx : Syntax) (acc : String) : String

def Lean.Elab.Command.mkNameFromParserSyntax.appendCatName (catName : Name) (str : String) : String

def Lean.Elab.Command.resolveSyntaxKind (k : Name) : CommandElabM Name

def Lean.Elab.Command.isLocalAttrKind (attrKind : Syntax) : Bool

def Lean.Elab.Command.addMacroScopeIfLocal {m : Type → Type} [MonadQuotation m] [Monad m] (name : Name) (attrKind : Syntax) : m Name

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

def Lean.Elab.Command.elabSyntax : CommandElab

def Lean.Elab.Command.elabSyntaxAbbrev : CommandElab

def Lean.Elab.Command.checkRuleKind (given expected : SyntaxNodeKind) : Bool

def Lean.Elab.Command.inferMacroRulesAltKind : TSyntax `Lean.Parser.Term.matchAlt → CommandElabM SyntaxNodeKind

def Lean.Elab.Command.expandNoKindMacroRulesAux (alts : Array (TSyntax `Lean.Parser.Term.matchAlt)) (cmdName : String) (mkCmd : Option Name → Array (TSyntax `Lean.Parser.Term.matchAlt) → CommandElabM Command) : CommandElabM Command

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.

def Lean.Elab.Command.strLitToPattern (stx : Syntax) : MacroM Syntax