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

Equations

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

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

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

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

def Lean.Elab.Tactic.Conv.PatternMatchState.isDone : Lean.Elab.Tactic.Conv.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

def Lean.Elab.Tactic.Conv.PatternMatchState.isReady : Lean.Elab.Tactic.Conv.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

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

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

def Lean.Elab.Tactic.Conv.PatternMatchState.accept (mvarId : Lean.MVarId) : Lean.Elab.Tactic.Conv.PatternMatchState → Lean.Elab.Tactic.Conv.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

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

Equations

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