Forked from
Iris / Iris
Source project has a limited visibility.
-
Paolo G. Giarrusso authored
Debatable, but the proof context of `na_inv_alloc` writes `ε` instead of `CoPSet ∅`.
Paolo G. Giarrusso authoredDebatable, but the proof context of `na_inv_alloc` writes `ε` instead of `CoPSet ∅`.