program_logic/model.v · c7240c72617b794a03267d2c6ceba3d0acbdbed0 · Abhishek Anand / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago
e9e55145
Turn iProp into a notation. · e9e55145
Robbert Krebbers authored 8 years ago
```
This avoids Coq distinguishing iProp and uPred (iResUR _) when it
should not.
```
e9e55145

History
Turn iProp into a notation.
Robbert Krebbers authored 8 years ago
```
This avoids Coq distinguishing iProp and uPred (iResUR _) when it
should not.
```