Worklist driver for mvcgen'. Wraps solve with a queue of pending goals, emits VCs (or invariant holes) for those solve cannot decompose further, and runs the user-configured preTac on each emitted VC.

def Lean.Elab.Tactic.Do.Internal.VCGen.PreTac.run : PreTac → Meta.Grind.Goal → VCGenM (List Meta.Grind.Goal)

Runs the preTac on the VC:

• .grind: tries to solve the VC using the accumulated Grind.Goal state via Grind.Goal.grind. Reports failure via Lean.logError unless silent is set.
• .tactic: runs the user-provided tactic on the VC, potentially emitting multiple subgoals.
• .none: returns the VC as-is.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Do.Internal.VCGen.PreTac.none.run x✝ = pure [x✝]

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

• preTacFailed : Bool

  True iff some non-silent pre-tactic failed during VC generation.

def Lean.Elab.Tactic.Do.Internal.VCGen.run (goal : Meta.Grind.Goal) (ctx : Context) (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.