Sebastian Graf c6689584ea fix: split ifs in mvcgen rather than relying on a spec (#9176) ... This PR makes `mvcgen` split ifs rather than applying specifications. Doing so fixes a bug reported by Rish. Co-authored-by: Sebastian Graf <sg@lean-fro.org>		2025-07-03 14:29:17 +00:00
..
SPred	fix: More fixes for Std.Do accumulated while merging tests (#9038)	2025-06-27 13:10:43 +00:00
Triple	fix: split ifs in mvcgen rather than relying on a spec (#9176)	2025-07-03 14:29:17 +00:00
WP	feat: Hoare logic for monadic programs and verification condition generation (#8995)	2025-06-26 15:49:56 +00:00
PostCond.lean	fix: Use fullApproxDefEq in mspec to fix a bug reported by Rish (#9041)	2025-06-27 14:31:39 +00:00
PredTrans.lean	feat: Hoare logic for monadic programs and verification condition generation (#8995)	2025-06-26 15:49:56 +00:00
SPred.lean	feat: Upstream MPL.SPred.* from mpl (#8928)	2025-06-26 11:15:11 +00:00
Triple.lean	feat: Hoare logic for monadic programs and verification condition generation (#8995)	2025-06-26 15:49:56 +00:00
WP.lean	feat: Hoare logic for monadic programs and verification condition generation (#8995)	2025-06-26 15:49:56 +00:00