## Equations

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

## Instances For

- all: Array Lean.MVarId → Lean.Elab.Tactic.Conv.PatternMatchState
The state corresponding to a

`(occs := *)`

pattern, which acts like`occs := 1 2 ... n`

where`n`

is the total number of pattern matches.`subgoals`

is the list of subgoals for patterns already matched

- occs: Array (Nat × Lean.MVarId) → Nat → List (Nat × Nat) → Lean.Elab.Tactic.Conv.PatternMatchState
The state corresponding to a partially consumed

`(occs := a₁ a₂ ...)`

pattern.`subgoals`

is the list of subgoals for patterns already matched, along with their index in the original occs list`idx`

is the number of matches that have occurred so far`remaining`

is a list of`(i, orig)`

pairs representing matches we have not yet reached. We maintain the invariant that`idx :: remaining.map (·.1)`

is sorted. The number`i`

is the value in the`occs`

list and`orig`

is its index in the list.

## Instances For

Is this pattern no longer interested in accepting matches?

## Equations

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

## Instances For

Is this pattern interested in accepting the next match?

## Equations

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

## Instances For

Assuming `isReady`

returned false, this advances to the next match.

## Equations

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

## Instances For

Assuming `isReady`

returned true, this adds the generated subgoal to the list
and advances to the next match.

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