Equations
- One or more equations did not get rendered due to their size.
- all: Array Lean.MVarId → Lean.Elab.Tactic.Conv.PatternMatchState
The state corresponding to a
(occs := *)
pattern, which acts likeoccs := 1 2 ... n
wheren
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 listidx
is the number of matches that have occurred so farremaining
is a list of(i, orig)
pairs representing matches we have not yet reached. We maintain the invariant thatidx :: remaining.map (·.1)
is sorted. The numberi
is the value in theoccs
list andorig
is its index in the list.
Is this pattern no longer interested in accepting matches?
Equations
- (Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals).isDone = false
- (Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals idx remaining).isDone = remaining.isEmpty
Is this pattern interested in accepting the next match?
Equations
- (Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals).isReady = true
- (Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals idx ((i, snd) :: tail)).isReady = (idx == i)
- x.isReady = false
Assuming isReady
returned false, this advances to the next match.
Equations
- (Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals idx remaining).skip = Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals (idx + 1) remaining
- x.skip = x
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.
- Lean.Elab.Tactic.Conv.PatternMatchState.accept mvarId (Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals) = Lean.Elab.Tactic.Conv.PatternMatchState.all (subgoals.push mvarId)
- Lean.Elab.Tactic.Conv.PatternMatchState.accept mvarId x = x
Equations
- One or more equations did not get rendered due to their size.