Forked from
Iris / Iris
5002 commits behind the upstream repository.
Jacques-Henri Jourdan
authored
(□ P) now means (bi_bare (bi_persistently P)). This is motivated by the fact that these two modalities are rarely used separately. In the case of an affine BI, we keep the □ notation. This means that a bi_bare is inserted each time we use □. Hence, a few adaptations need to be done in the proof mode class instances.
| Name | Last commit | Last update |
|---|---|---|
| .. | ||
| adequacy.v | ||
| ectx_language.v | ||
| ectx_lifting.v | ||
| ectxi_language.v | ||
| hoare.v | ||
| language.v | ||
| lifting.v | ||
| ownp.v | ||
| weakestpre.v | ||