Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
Instead of having connectives pvs0 and pvs1 we now have one connective pvs that is indexed by a Boolean.
Robbert Krebbers authoredInstead of having connectives pvs0 and pvs1 we now have one connective pvs that is indexed by a Boolean.
