partial def Lean.Elab.Term.Quotation.mkTuple : Array Syntax → TermElabM Syntax

def Lean.Elab.Term.Quotation.resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name × List String)

def Lean.Elab.Term.Quotation.resolveSectionVariable.loop (sectionVars : NameMap Name) (extractionResult : MacroScopesView) : Name → List String → List (Name × List String)

def Lean.Elab.Term.Quotation.ArrayStxBuilder : Type

Transform sequence of pushes and appends into acceptable code

def Lean.Elab.Term.Quotation.ArrayStxBuilder.empty : ArrayStxBuilder

def Lean.Elab.Term.Quotation.ArrayStxBuilder.build : ArrayStxBuilder → Term

def Lean.Elab.Term.Quotation.ArrayStxBuilder.push (b : ArrayStxBuilder) (elem : Syntax) : ArrayStxBuilder

def Lean.Elab.Term.Quotation.ArrayStxBuilder.append (b : ArrayStxBuilder) (arr : Syntax) (appendName : Name := `Array.append) : ArrayStxBuilder

def Lean.Elab.Term.Quotation.ArrayStxBuilder.mkNode (b : ArrayStxBuilder) (k : SyntaxNodeKind) : TermElabM Term

def Lean.Elab.Term.Quotation.tryAddSyntaxNodeKindInfo (stx : Syntax) (k : SyntaxNodeKind) : TermElabM Unit

instance Lean.Elab.Term.Quotation.instQuotePreresolvedMkStr1_lean : Quote Syntax.Preresolved

def Lean.Elab.Term.Quotation.addNamedQuotInfo (stx : Syntax) (k : SyntaxNodeKind) : TermElabM SyntaxNodeKind

def Lean.Elab.Term.Quotation.getQuotKind (stx : Syntax) : TermElabM SyntaxNodeKind

def Lean.Elab.Term.Quotation.mkSyntaxQuotation (stx : Syntax) (kind : Name) : TermElabM Syntax

def Lean.Elab.Term.Quotation.stxQuot.expand (stx : Syntax) : TermElabM Syntax

def Lean.Elab.Term.Quotation.commandElab_stx_quot_ : ParserDescr

match

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

• unconditional : HeadCheck

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

• shape (k : List SyntaxNodeKind) (arity : Option Nat) : 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

• slice (numPrefix numSuffix : Nat) : 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`

• other (pat : Syntax) : HeadCheck

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

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

• covered (f : Lean.Elab.Term.Quotation.Alt✝ → TermElabM Lean.Elab.Term.Quotation.Alt✝) (exhaustive : Bool) : MatchResult

  Pattern agrees with head check, remove and transform remaining alternative. If exhaustive is false, also include unchanged alternative in the "no" branch.

• uncovered : MatchResult

  Pattern disagrees with head check, include in "no" branch only

• undecided : MatchResult

  Pattern is not quite sure yet; include unchanged in both branches

instance Lean.Elab.Term.Quotation.instReprMatchResult : Repr MatchResult

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

All necessary information on a pattern head.

• check : HeadCheck

  check induced by the pattern

• onMatch (taken : HeadCheck) : MatchResult

  compute compatibility of pattern with given head check

• doMatch (yes : List Term → TermElabM Term) (no : TermElabM Term) : TermElabM Term

  actually run the specified head check, with the discriminant bound to __discr

@[reducible, inline]

abbrev Lean.Elab.Term.Quotation.IdxSet : Type

def Lean.Elab.Term.Quotation.match_syntax.expand (stx : Syntax) : TermElabM Syntax

def Lean.Elab.Term.Quotation.elabMatchSyntax : TermElab

def Lean.Elab.Term.Quotation.elabNoErrorIfUnused : TermElab