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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.Quotation.resolveSectionVariable.loop sectionVars extractionResult x x = []

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

Transform sequence of pushes and appends into acceptable code

Equations

• Lean.Elab.Term.Quotation.ArrayStxBuilder = (Array Lean.Term ⊕ Lean.Term)

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

Equations

• Lean.Elab.Term.Quotation.ArrayStxBuilder.empty = Sum.inl #[]

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

Equations

• Lean.Elab.Term.Quotation.ArrayStxBuilder.build x = match x with | Sum.inl elems => Lean.quote `term elems | Sum.inr arr => arr

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.

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

Equations

• Lean.Elab.Term.Quotation.ArrayStxBuilder.append b arr appendName = Sum.inr (Lean.Syntax.mkCApp appendName #[Lean.Elab.Term.Quotation.ArrayStxBuilder.build b, { raw := arr }])

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.

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.

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

Equations

• One or more equations did not get rendered due to their size.

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.

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.

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

Equations

• One or more equations did not get rendered due to their size.

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.

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

Equations

• One or more equations did not get rendered due to their size.

match

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

• unconditional: Lean.Elab.Term.Quotation.HeadCheck

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

• shape: List Lean.SyntaxNodeKind → Option Nat → 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

• slice: Nat → 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`

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

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

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

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

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

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

• uncovered: Lean.Elab.Term.Quotation.MatchResult

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

• undecided: Lean.Elab.Term.Quotation.MatchResult

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

• check : Lean.Elab.Term.Quotation.HeadCheck

  check induced by the pattern

• onMatch : Lean.Elab.Term.Quotation.HeadCheck → Lean.Elab.Term.Quotation.MatchResult

  compute compatibility of pattern with given head check

• doMatch : (List Lean.Term → Lean.Elab.TermElabM Lean.Term) → Lean.Elab.TermElabM Lean.Term → Lean.Elab.TermElabM Lean.Term

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

All necessary information on a pattern head.

@[inline, reducible]

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

Equations

• Lean.Elab.Term.Quotation.IdxSet = Lean.HashSet Nat

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.

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

Equations

• Lean.Elab.Term.Quotation.elabMatchSyntax = Lean.Elab.Term.adaptExpander Lean.Elab.Term.Quotation.match_syntax.expand

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

Equations

• One or more equations did not get rendered due to their size.