# Documentation

Lean.Parser.Extension

Extensible parsing via attributes

Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
@[inline]
Equations
def Lean.Parser.addLeadingParser (categories : Lean.Parser.ParserCategories) (catName : Lean.Name) (declName : Lean.Name) (p : Lean.Parser.Parser) (prio : Nat) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.addTrailingParser (categories : Lean.Parser.ParserCategories) (catName : Lean.Name) (declName : Lean.Name) (prio : Nat) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.addParser (categories : Lean.Parser.ParserCategories) (catName : Lean.Name) (declName : Lean.Name) (leading : Bool) (p : Lean.Parser.Parser) (prio : Nat) :
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.
inductive Lean.Parser.AliasValue (α : Type) :
• const: {α : Type} →
• unary: {α : Type} → (αα) →
• binary: {α : Type} → (ααα) →

Parser aliases for making ParserDescr extensible

Instances For
@[inline]
Equations
def Lean.Parser.registerAliasCore {α : Type} (mapRef : ) (aliasName : Lean.Name) (value : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.getAlias {α : Type} (mapRef : ) (aliasName : Lean.Name) :
Equations
def Lean.Parser.getConstAlias {α : Type} (mapRef : ) (aliasName : Lean.Name) :
IO α
Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.getUnaryAlias {α : Type} (mapRef : ) (aliasName : Lean.Name) :
IO (αα)
Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.getBinaryAlias {α : Type} (mapRef : ) (aliasName : Lean.Name) :
IO (ααα)
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
• declName : Lean.Name
• Number of syntax nodes produced by this parser. none means "sum of input sizes".

stackSz? :
• Whether arguments should be wrapped in group(·) if they do not produce exactly one syntax node.

autoGroupArgs : Bool
Instances For
Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.registerAlias (aliasName : Lean.Name) (declName : Lean.Name) (kind? : ) (info : optParam Lean.Parser.ParserAliasInfo { declName := Lean.Name.anonymous, stackSz? := some 1, autoGroupArgs := }) :
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
Equations
unsafe def Lean.Parser.mkParserOfConstantUnsafe (constName : Lean.Name) (compileParserDescr : ) :
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by Lean.Parser.mkParserOfConstantUnsafe]
opaque Lean.Parser.mkParserOfConstantAux (constName : Lean.Name) (compileParserDescr : ) :
• Called after a parser attribute is applied to a declaration.

Instances For
Equations
def Lean.Parser.runParserAttributeHooks (catName : Lean.Name) (declName : Lean.Name) (builtin : Bool) :
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.
@[implemented_by Lean.Parser.evalParserConstUnsafe]

Run declName if possible and inside a quotation, or else p. The ParserInfo will always be taken from p.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.addBuiltinParser (catName : Lean.Name) (declName : Lean.Name) (leading : Bool) (p : Lean.Parser.Parser) (prio : Nat) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.addBuiltinLeadingParser (catName : Lean.Name) (declName : Lean.Name) (p : Lean.Parser.Parser) (prio : Nat) :
Equations
def Lean.Parser.addBuiltinTrailingParser (catName : Lean.Name) (declName : Lean.Name) (prio : Nat) :
Equations
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
Equations
Equations
Equations
def Lean.Parser.runParserCategory (env : Lean.Environment) (catName : Lean.Name) (input : String) (fileName : optParam String "<input>") :

convenience function for testing

Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.declareBuiltinParser (addFnName : Lean.Name) (catName : Lean.Name) (declName : Lean.Name) (prio : Nat) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.declareLeadingBuiltinParser (catName : Lean.Name) (declName : Lean.Name) (prio : Nat) :
Equations
def Lean.Parser.declareTrailingBuiltinParser (catName : Lean.Name) (declName : Lean.Name) (prio : Nat) :
Equations
Equations
• One or more equations did not get rendered due to their size.

The parsing tables for builtin parsers are "stored" in the extracted source code.

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.

A builtin parser attribute that can be extended by users.

Equations
def Lean.Parser.registerParserCategory (env : Lean.Environment) (attrName : Lean.Name) (catName : Lean.Name) (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.

If the parsing stack is of the form #[.., openCommand], we process the open command, and execute p

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

If the parsing stack is of the form #[.., openDecl], we process the open declaration, and execute p

Equations
• One or more equations did not get rendered due to their size.
• category:
• parser:
Instances For
def Lean.Parser.resolveParserNameCore (env : Lean.Environment) (currNamespace : Lean.Name) (openDecls : ) (ident : Lean.Ident) :

Resolve the given parser name and return a list of candidates.

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.

Resolve the given parser name and return a list of candidates.

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

Resolve the given parser name and return a list of candidates.

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.