Documentation

Lean.Elab.Syntax

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

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

Equations
source
structure Lean.Elab.Term.ToParserDescrContext :
Type
source
@[reducible, inline]
abbrev Lean.Elab.Term.ToParserDescrM (α : Type) :
Type
Equations
source
@[reducible, inline]
abbrev Lean.Elab.Term.ToParserDescr :
Type
Equations
source
def Lean.Elab.Term.ensureUnaryOutput (x : Term × Nat) :
Term
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.addCategoryInfo (ref : Syntax) (catName : Name) :
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.
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.checkLeftRec (stx : Syntax) :
ToParserDescrM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.elabParserName? (stx : Ident) :
TermElabM (Option Parser.ParserResolution)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.elabParserName (stx : Ident) :
TermElabM Parser.ParserResolution
Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Term.toParserDescr.process (stx : Syntax) :
ToParserDescr
source
partial def Lean.Elab.Term.toParserDescr.processSeq (stx : Syntax) :
ToParserDescrM (Term × Nat)

Sequence (aka NullNode)

source
def Lean.Elab.Term.toParserDescr.ensureNoPrec (stx : Syntax) :
ToParserDescrM PUnit
Equations
source
def Lean.Elab.Term.toParserDescr.processParserCategory (stx : Syntax) :
ToParserDescrM (Term × Nat)
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Term.toParserDescr.processAlias (id : Syntax) (args : Array Syntax) :
ToParserDescrM (Term × Nat)
source
partial def Lean.Elab.Term.toParserDescr.processNullaryOrCat (stx : Syntax) :
ToParserDescrM (Term × Nat)
source
partial def Lean.Elab.Term.toParserDescr.processSepBy (stx : Syntax) :
ToParserDescrM (Term × Nat)
source
partial def Lean.Elab.Term.toParserDescr.processSepBy1 (stx : Syntax) :
ToParserDescrM (Term × Nat)
source
def Lean.Elab.Term.toParserDescr.isValidAtom (s : String) :
Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.toParserDescr.processAtom (stx : Syntax) :
ToParserDescrM (Term × Nat)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.toParserDescr.processNonReserved (stx : Syntax) :
ToParserDescrM (Term × Nat)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabDeclareSyntaxCat :
CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
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[_,]

Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Command.mkNameFromParserSyntax.visit (stx : Syntax) (acc : String) :
String
source
def Lean.Elab.Command.mkNameFromParserSyntax.appendCatName (catName : Name) (str : String) :
String
Equations
source
def Lean.Elab.Command.resolveSyntaxKind (k : Name) :
CommandElabM Name
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.isLocalAttrKind (attrKind : Syntax) :
Bool
Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabSyntax :
CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabSyntaxAbbrev :
CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.checkRuleKind (given expected : SyntaxNodeKind) :
Bool
Equations
source
def Lean.Elab.Command.inferMacroRulesAltKind :
TSyntax `Lean.Parser.Term.matchAlt → CommandElabM SyntaxNodeKind
Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.strLitToPattern (stx : Syntax) :
MacroM Syntax
Equations