Worklist driver for mvcgen'. Wraps solve with a queue of pending goals and emits VCs (or invariant holes) for those solve cannot decompose further.

def Lean.Elab.Tactic.Do.Internal.VCGen.elabInvariant (invariantAlts : Std.HashMap Nat Syntax) (n : Nat) (mv : MVarId) : Meta.Sym.SymM Bool

Try to elaborate the user's invariant alt for invariant number n inline, discharging mv if successful. Looks up Context.invariantAlts[n]? (pre-parsed in Frontend) and dispatches to exact $rhs for bullet form or rename_i $args*; exact $rhs for labelled form. Returns whether elaboration succeeded. Numbering is 1-based; out-of-order labelled forms (e.g. | inv2 => … before | inv1 => …) are supported because the map is keyed by parsed number, not position.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.emitVC (goal : Meta.Grind.Goal) : VCGenM Unit

Called when decomposing the goal further did not succeed; in this case we emit a VC for the goal. Invariant subgoals are handled separately by handleInvariantSubgoals directly inside work, so they never reach this path.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.work (scope : Scope) (goal : Meta.Grind.Goal) : VCGenM Unit

Equations

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

structure Lean.Elab.Tactic.Do.Internal.VCGen.Result : Type

• invariants : Array MVarId

  All invariant goals emitted during VC generation, in emit order. The MVarId at index i carries tag inv{i+1}, so callers can treat the array index as the invariant number. Some entries may already be assigned (inline-elaborated by Driver.emitVC); the caller is responsible for filtering before discharging.

• vcs : Array Meta.Grind.Goal

  Unassigned VCs. Each shares the parent Grind.Goal's state.

• inlineHandledInvariants : Std.HashSet Nat

  Invariant numbers handled inline by Driver.emitVC. Used by Frontend to avoid spurious "alt does not match any invariant" warnings for inline-consumed alts.

def Lean.Elab.Tactic.Do.Internal.VCGen.run (goal : Meta.Grind.Goal) (ctx : Context) (scope : Scope) (stepLimit? : Option Nat := none) : Meta.Grind.GrindM Result

Generate verification conditions for a goal of the form P ⊢ₛ wp⟦e⟧ Q s₁ ... sₙ by repeatedly decomposing e using registered @[spec] theorems. Return the VCs and invariant goals.

stepLimit?, when some n, seeds the fuel counter to n; when none, fuel is unlimited.

Equations

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