Documentation

Lean.Elab.Tactic.Conv.Pattern

source
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.
source
partial def Lean.Elab.Tactic.Conv.matchPattern?.go? (pattern : Lean.Expr) (e : Lean.Expr) :
Lean.MetaM (Option (Lean.Expr × Array Lean.Expr))
source
inductive Lean.Elab.Tactic.Conv.PatternMatchState :
Type

  • 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
    all: Array Lean.MVarId → 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.
    occs: Array (Nat × Lean.MVarId) → Nat → List (Nat × Nat) → Lean.Elab.Tactic.Conv.PatternMatchState
Instances For
    source
    def Lean.Elab.Tactic.Conv.PatternMatchState.isDone :
    Lean.Elab.Tactic.Conv.PatternMatchState → Bool

    Is this pattern no longer interested in accepting matches?

    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Lean.Elab.Tactic.Conv.PatternMatchState.isReady :
    Lean.Elab.Tactic.Conv.PatternMatchState → Bool

    Is this pattern interested in accepting the next match?

    Equations
    • One or more equations did not get rendered due to their size.
    source
    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
    • One or more equations did not get rendered due to their size.
    source
    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.
    source
    def Lean.Elab.Tactic.Conv.evalPattern :
    Lean.Elab.Tactic.Tactic
    Equations
    • One or more equations did not get rendered due to their size.