Open JonasAlaif opened 1 week ago
Making a note that this is an error from the flycheck: with verification enabled we do not get the error.
I can no longer reproduce this with the recent changes to the matcher. FWIW, the vscode extension now discards errors from the flycheck process if we've already checked the top-level definition using the main process, and errors from the flycheck process are shown as warnings.
This PR made this particular issue go away, but this one still shows a spurious error for me (flycheck fails on cond_lemma, normal mode fails on the assert):
```pulse
fn fold_pre
(b: bool)
(y: vprop)
requires (if b then emp else y)
ensures (if b then emp else y)
{
assert (pure False);
if not (b) {
assert (pure (not (b)));
cond_lemma #b #emp #y;
} else {
()
}
}
let _ = assert False
I think https://github.com/FStarLang/FStar/pull/3337 would solve it, at the cost of verifying the Pulse fragment twice (one for each process). Until we maybe add flychecking support to the Pulse checker as we discussed today.
Relabeling this issue.
In the following snippet
I get the error
If I comment out the assert, the error goes away.