Documentation

Lean.Elab.Tactic.Conv.Pattern

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    • all: Array Lean.MVarIdLean.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)NatList (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.
    Instances For

      Is this pattern no longer interested in accepting matches?

      Equations
      Instances For

        Is this pattern interested in accepting the next match?

        Equations
        Instances For

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

          Equations
          Instances For

            Assuming isReady returned true, this adds the generated subgoal to the list and advances to the next match.

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