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

partial def Lean.Elab.Tactic.Conv.matchPattern?.go? (pattern e : Expr) : MetaM (Option (Expr × Array Expr))

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.

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

Is this pattern no longer interested in accepting matches?

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

Is this pattern interested in accepting the next match?

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

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

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.

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