Documentation

Lean.Elab.Quotation

source
partial def Lean.Elab.Term.Quotation.mkTuple:
Array Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax
source
def Lean.Elab.Term.Quotation.resolveSectionVariable (sectionVars : Lean.NameMap Lean.Name) (id : Lean.Name) :
List (Lean.Name × List String)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.Quotation.resolveSectionVariable.loop (sectionVars : Lean.NameMap Lean.Name) (extractionResult : Lean.MacroScopesView) :
Lean.Name → List String → List (Lean.Name × List String)
Equations
source
def Lean.Elab.Term.Quotation.ArrayStxBuilder:
Type

Transform sequence of pushes and appends into acceptable code

Equations
source
def Lean.Elab.Term.Quotation.ArrayStxBuilder.empty:
Lean.Elab.Term.Quotation.ArrayStxBuilder
Equations
source
def Lean.Elab.Term.Quotation.ArrayStxBuilder.build:
Lean.Elab.Term.Quotation.ArrayStxBuilder → Lean.Term
Equations
source
def Lean.Elab.Term.Quotation.ArrayStxBuilder.push (b : Lean.Elab.Term.Quotation.ArrayStxBuilder) (elem : Lean.Syntax) :
Lean.Elab.Term.Quotation.ArrayStxBuilder
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.Quotation.ArrayStxBuilder.append (b : Lean.Elab.Term.Quotation.ArrayStxBuilder) (arr : Lean.Syntax) (appendName : optParam Lean.Name `Array.append) :
Lean.Elab.Term.Quotation.ArrayStxBuilder
Equations
source
def Lean.Elab.Term.Quotation.getQuotKind (stx : Lean.Syntax) :
Lean.Elab.TermElabM Lean.SyntaxNodeKind
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.Quotation.stxQuot.expand (stx : Lean.Syntax) :
Lean.Elab.TermElabM Lean.Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.Quotation.commandElab_stx_quot_:
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
inductive Lean.Elab.Term.Quotation.HeadCheck:
Type

In a single match step, we match the first discriminant against the "head" of the first pattern of the first alternative. This datatype describes what kind of check this involves, which helps other patterns decide if they are covered by the same check and don't have to be checked again (see also MatchResult).

source
inductive Lean.Elab.Term.Quotation.MatchResult:
Type

Describe whether a pattern is covered by a head check (induced by the pattern itself or a different pattern).

source
structure Lean.Elab.Term.Quotation.HeadInfo:
Type

All necessary information on a pattern head.

source
def Lean.Elab.Term.Quotation.match_syntax.expand (stx : Lean.Syntax) :
Lean.Elab.TermElabM Lean.Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.Quotation.elabMatchSyntax:
Lean.Elab.Term.TermElab

Syntactic pattern match. Matches a Syntax value against quotations, pattern variables, or _.

Equations