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.ArrayStxBuilder.mkNode (b : Lean.Elab.Term.Quotation.ArrayStxBuilder) (k : Lean.SyntaxNodeKind) :
Lean.Elab.TermElabM Lean.Term
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.Quotation.tryAddSyntaxNodeKindInfo (stx : Lean.Syntax) (k : Lean.SyntaxNodeKind) :
Lean.Elab.TermElabM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Elab.Term.Quotation.instQuotePreresolvedMkStr1 :
Lean.Quote Lean.Syntax.Preresolved
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Term.Quotation.addNamedQuotInfo (stx : Lean.Syntax) (k : Lean.SyntaxNodeKind) :
Lean.Elab.TermElabM Lean.SyntaxNodeKind
Equations
  • One or more equations did not get rendered due to their size.
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.mkSyntaxQuotation (stx : Lean.Syntax) (kind : Lean.Name) :
Lean.Elab.TermElabM Lean.Syntax
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.

match #

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

  • match step that always succeeds: _, x, `($x), ...

    unconditional: Lean.Elab.Term.Quotation.HeadCheck

  • match step based on kind and, optionally, arity of discriminant If arity is given, that number of new discriminants is introduced. covered patterns should then introduce the same number of new patterns. We actually check the arity at run time only in the case of null nodes since it should otherwise by implied by the node kind. without arity: `($x:k) with arity: any quotation without an antiquotation head pattern

    shape: List Lean.SyntaxNodeKind → Option Nat → Lean.Elab.Term.Quotation.HeadCheck

  • Match step that succeeds on null nodes of arity at least numPrefix + numSuffix, introducing discriminants for the first numPrefix children, one null node for those in between, and for the numSuffix last children. example: ([$x, $xs,*, $y]) is slice 2 2`

    slice: Nat → Nat → Lean.Elab.Term.Quotation.HeadCheck

  • other, complicated match step that will probably only cover identical patterns example: antiquotation splices `($[...]*)

    other: Lean.Syntax → Lean.Elab.Term.Quotation.HeadCheck

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

Instances For
    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).

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

      All necessary information on a pattern head.

      Instances For
        source
        @[inline]
        abbrev Lean.Elab.Term.Quotation.IdxSet :
        Type
        Equations
        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
        Equations
        source
        def Lean.Elab.Term.Quotation.elabNoErrorIfUnused :
        Lean.Elab.Term.TermElab
        Equations
        • One or more equations did not get rendered due to their size.