mvcgen' 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 mvcgen', 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.elabMVCGen' : Tactic

Tactic-level mvcgen'. Reuses the grind-mode implementation by re-quoting the input as Grind.mvcgen' … 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 mvcgen'.

Equations

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