Skip to content
Snippets Groups Projects
Forked from Iris / Iris
Source project has a limited visibility.
user avatar
Robbert Krebbers authored
This commit introduces the following soundness statements:

- Soundness of pure propositions `⌜ φ ⌝%I → φ`.
- Soundness of later `(▷ P)%I → P`.

The old soundness statement, `(▷^n ⌜ φ ⌝)%I → φ` is now a derived form.
473ad60b
History
Name Last commit Last update