Documentation

Lean.Elab.Syntax

source
def Lean.Elab.Term.expandOptPrecedence (stx : Lean.Syntax) :
Lean.MacroM (Option Nat)
Equations
source
structure Lean.Elab.Term.ToParserDescrContext:
Type
source
@[inline]
abbrev Lean.Elab.Term.ToParserDescrM (α : Type) :
Type
Equations
source
@[inline]
abbrev Lean.Elab.Term.ToParserDescr:
Type
Equations
source
def Lean.Elab.Term.ensureUnaryOutput (x : Lean.Term × Nat) :
Lean.Term
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
def Lean.Elab.Term.resolveParserName {m : Type → Type} [inst : Monad m] [inst : Lean.Elab.MonadInfoTree m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (parserName : Lean.Syntax) :
m (List (Lean.Name × Bool))

Resolve the given parser name and return a list of candidates. Each candidate is a pair (resolvedParserName, isDescr). isDescr == true if the type of resolvedParserName is a ParserDescr.

Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
partial def Lean.Elab.Term.toParserDescr.process (stx : Lean.Syntax) :
Lean.Elab.Term.ToParserDescr
source
partial def Lean.Elab.Term.toParserDescr.processSeq (stx : Lean.Syntax) :
Lean.Elab.Term.ToParserDescrM (Lean.Term × Nat)
source
def Lean.Elab.Term.toParserDescr.ensureNoPrec (stx : Lean.Syntax) :
Lean.Elab.Term.ToParserDescrM PUnit
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
partial def Lean.Elab.Term.toParserDescr.processAlias (id : Lean.Syntax) (args : Array Lean.Syntax) :
Lean.Elab.Term.ToParserDescrM (Lean.Term × Nat)
source
partial def Lean.Elab.Term.toParserDescr.processNullaryOrCat (stx : Lean.Syntax) :
Lean.Elab.Term.ToParserDescrM (Lean.Term × Nat)
source
partial def Lean.Elab.Term.toParserDescr.processSepBy (stx : Lean.Syntax) :
Lean.Elab.Term.ToParserDescrM (Lean.Term × Nat)
source
partial def Lean.Elab.Term.toParserDescr.processSepBy1 (stx : Lean.Syntax) :
Lean.Elab.Term.ToParserDescrM (Lean.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 : Lean.Syntax) :
Lean.Elab.Term.ToParserDescrM (Lean.Term × Nat)
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
def Lean.Elab.Command.elabDeclareSyntaxCat:
Lean.Elab.Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
partial def Lean.Elab.Command.mkNameFromParserSyntax.visit (stx : Lean.Syntax) (acc : String) :
String
source
def Lean.Elab.Command.mkNameFromParserSyntax.appendCatName (catName : Lean.Name) (str : String) :
String
Equations
source
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.
source
def Lean.Elab.Command.elabSyntax:
Lean.Elab.Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabSyntaxAbbrev:
Lean.Elab.Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.checkRuleKind (given : Lean.SyntaxNodeKind) (expected : Lean.SyntaxNodeKind) :
Bool
Equations
source
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.
source
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.
source
def Lean.Elab.Command.strLitToPattern (stx : Lean.Syntax) :
Lean.MacroM Lean.Syntax
Equations