## Equations

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

## Instances For

## Equations

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

## Instances For

Transform sequence of pushes and appends into acceptable code

## Instances For

## Equations

- x.build = match x with | Sum.inl elems => Lean.quote elems | Sum.inr arr => arr

## Instances For

## Equations

## Instances For

## Equations

- b.append arr appendName = Sum.inr (Lean.Syntax.mkCApp appendName #[b.build, { raw := arr }])

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

# match #

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: 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 `($[...]*)

## Instances For

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

- 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

## Instances For

## Equations

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

All necessary information on a pattern head.

check induced by the pattern

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`

## Instances For

## Equations

## Instances For

## Equations

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

## Instances For

## Equations

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