Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
This allows us to factor out properties about connectives that commute with the big operators.
Robbert Krebbers authoredThis allows us to factor out properties about connectives that commute with the big operators.