Skip to content

fix(phl): require the invariant on loop entry in the while variant rule - #1132

Open
Yiping106283 wants to merge 1 commit into
EasyCrypt:mainfrom
Yiping106283:fix-phoare-while-variant-entry
Open

fix(phl): require the invariant on loop entry in the while variant rule#1132
Yiping106283 wants to merge 1 commit into
EasyCrypt:mainfrom
Yiping106283:fix-phoare-while-variant-entry

fix(phl): require the invariant on loop entry in the `while` variant …

b616c7a
Select commit
Loading
Failed to load commit list.
Sign in for the full log view