feat: new foundations for `mvcgen` tactic#12965

Open

volodeyka wants to merge 32 commits intomasterfrom

vova/new-do-foundations

Commits on Apr 16, 2026

add new mvcgen foundations
volodeyka
committed
remove some garbage
volodeyka
committed
add missing lemmas
volodeyka
committed
revert changes to toolchain
volodeyka
committed
Make AssertionLang/ExceptAssertionLang class abbrevs, pass as WPMonad args

volodeyka
and
claude
committed
Scope notations, move Frame to Lean.Order, rename inf_sup → meet_sup

volodeyka
and
claude
committed
Make EPost.nil/EPost.cons structures, simplify instances via PProd

volodeyka
and
claude
committed
PredTrans structure, rename WPMonad→WP, merge Assertion classes, add OptionT WP, remove dead code

volodeyka
and
claude
committed
more to new Std/Experimental folder
volodeyka
committed
rename WP to WPMonad
volodeyka
committed
remove redundant instance
volodeyka
committed
minimise import in Frame
volodeyka
committed
Refactor CompleteLattice.pure definition and simplify theorem statements by removing redundant attributes. Introduce `open Classical` for improved readability.
volodeyka
committed
add grind annotation
volodeyka
committed
Refactor loop invariant and exception invariant definitions in `SpecLemmas.lean`. Update documentation for clarity and consistency, replacing `EPred` with `eInvariant EPred` in relevant theorem sig…
volodeyka
committed
revert test_vcgen.lean to master version
volodeyka
committed

Commits on Apr 17, 2026