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 : Lean.Expr) (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

• x.isDone = match x with | Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals => false | Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals idx remaining => 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

• x.isReady = match x with | Lean.Elab.Tactic.Conv.PatternMatchState.all subgoals => true | Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals idx ((i, snd) :: tail) => idx == i | x => 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.

Equations

• x.skip = match x with | Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals idx remaining => Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals (idx + 1) remaining | s => s

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.

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

Equations

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