vcgen tactic frontend: parse the user-facing argument syntax into a VCGen.Context, run VCGen.run, and replace the main goal with the resulting invariants and VCs.

def Lean.Elab.Tactic.Do.Internal.VCGen.mkContext (lemmas : Syntax) (goal : MVarId) (ignoreStarArg : Bool := false) : TermElabM (Context × Scope)

Parse the optional [...] argument list for vcgen, partitioning entries into spec theorems and simp lemmas. Follows the same approach as Lean.Elab.Tactic.Do.VCGen.mkContext: each entry is first tried as a spec theorem, and on failure falls back to a simp/unfold lemma processed via mkSimpContext.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.inferProgType? (goalType : Expr) : MetaM (Option Expr)

Infer the program type of a vcgen goal, the key for frame-procedure selection and the expected type for elaborating frames/until patterns. Peels leading binders, then reads the program type from a bare wp … target, a pre ⊑ wp … entailment, or a Triple. When the program type is m α with m a WPMonad, the monad m is returned (frameprocs are keyed by monad); otherwise the whole program type is returned, so deep embeddings key on their own head. Returns none when the goal exposes no program.

Equations

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

def Lean.Elab.Tactic.Do.Internal.elabVCGen : Tactic

Tactic-level vcgen. Reuses the grind-mode implementation by re-quoting the input as Grind.vcgen … and running it inside a GrindTacticM context built without withProtectedMCtx, so leftover Grind.Goals flow back as the new tactic goals. The optional with $g:grind clause runs as <;> $g and lets the user-supplied grind step share an internalised E-graph with vcgen.

Equations

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