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.mkSpecContext (lemmas : Syntax) (goal : MVarId) (ignoreStarArg : Bool := false) : TermElabM Context

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.mkSpecContext: 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'.

Equations

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