# Documentation

Lean.Elab.Tactic.Conv.Pattern

Equations
• One or more equations did not get rendered due to their size.
• 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
all:
• 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.
occs:
Instances For

Is this pattern no longer interested in accepting matches?

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

Is this pattern interested in accepting the next match?

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

Assuming isReady returned false, this advances to the next match.

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

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.
Equations
• One or more equations did not get rendered due to their size.