theories/bi/derived_laws.v · 6c6d0d65b32d0d9c943031e9fa709c6c833d7ed1 · Gaëtan Gilbert / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

7 years ago
6c6d0d65
Weaken BI axiom `P ⊢ <pers> emp` into `emp ⊢ <pers> emp`. · 6c6d0d65
Robbert Krebbers authored 7 years ago
```
The old one is admissable.

Thanks to @jtassaro and @jung.
```
6c6d0d65

History
Weaken BI axiom `P ⊢ <pers> emp` into `emp ⊢ <pers> emp`.
Robbert Krebbers authored 7 years ago
```
The old one is admissable.

Thanks to @jtassaro and @jung.
```