source
def Lean.Elab.Tactic.Conv.matchPattern? (pattern : Meta.AbstractMVarsResult) (e : Expr) :
MetaM (Option (Expr × Array Expr))
Equations

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

Instances For

source
inductive Lean.Elab.Tactic.Conv.PatternMatchState :
Type

- all (subgoals : Array MVarId) : 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 (subgoals : Array (Nat × MVarId)) (idx : Nat) (remaining : List (Nat × Nat)) : 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

source
def Lean.Elab.Tactic.Conv.PatternMatchState.isDone :
PatternMatchState → Bool

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

Instances For

source
def Lean.Elab.Tactic.Conv.PatternMatchState.isReady :
PatternMatchState → Bool

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

Instances For

source
def Lean.Elab.Tactic.Conv.PatternMatchState.skip :
PatternMatchState → PatternMatchState

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✝

Instances For

source
def Lean.Elab.Tactic.Conv.PatternMatchState.accept (mvarId : MVarId) :
PatternMatchState → PatternMatchState

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✝

Instances For

source
def Lean.Elab.Tactic.Conv.evalPattern :
Tactic
Equations

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

Instances For