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

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

Equations

• Lean.Elab.Term.expandOptPrecedence stx = if Lean.Syntax.isNone stx = true then pure none else do let __do_lift ← Lean.evalPrec stx[0][1] pure (some __do_lift)

structure Lean.Elab.Term.ToParserDescrContext : Type

• catName : Lean.Name
• first : Bool
• leftRec : Bool

• See comment at Parser.ParserCategory.

  behavior : Lean.Parser.LeadingIdentBehavior

@[inline]

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

Equations

• Lean.Elab.Term.ToParserDescrM = ReaderT Lean.Elab.Term.ToParserDescrContext (StateRefT' IO.RealWorld (Option Nat) Lean.Elab.TermElabM)

@[inline]

abbrev Lean.Elab.Term.ToParserDescr : Type

Equations

• Lean.Elab.Term.ToParserDescr = Lean.Elab.Term.ToParserDescrM (Lean.Term × Nat)

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

Equations

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

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

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Term.toParserDescr (stx : Lean.Syntax) (catName : Lean.Name) : Lean.Elab.TermElabM (Lean.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.

Equations

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

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

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

Sequence (aka NullNode)

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

Equations

• Lean.Elab.Term.toParserDescr.ensureNoPrec stx = if Lean.Syntax.isNone stx[1] = true then pure PUnit.unit else Lean.throwErrorAt stx[1] (Lean.toMessageData "unexpected precedence")

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

Equations

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

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

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Command.elabDeclareSyntaxCat : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.mkNameFromParserSyntax (catName : Lean.Name) (stx : Lean.Syntax) : Lean.MacroM Lean.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[_,]

Equations

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

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

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

Equations

• Lean.Elab.Command.mkNameFromParserSyntax.appendCatName catName str = match catName with | Lean.Name.str pre s => s ++ str | x => str

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

Equations

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

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

Equations

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

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

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.

def Lean.Elab.Command.elabSyntax : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabSyntaxAbbrev : Lean.Elab.Command.CommandElab

Equations

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

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

Equations

• Lean.Elab.Command.checkRuleKind given expected = (given == expected || given == expected ++ `antiquot)

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

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 : Option Lean.Name → Array (Lean.TSyntax `Lean.Parser.Term.matchAlt) → Lean.Elab.Command.CommandElabM Lean.Command) : Lean.Elab.Command.CommandElabM Lean.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.

Equations

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

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

Equations

• Lean.Elab.Command.strLitToPattern stx = match Lean.Syntax.isStrLit? stx with | some str => pure (Lean.mkAtomFrom stx str) | none => Lean.Macro.throwUnsupported