Forked from
Iris / Iris
Source project has a limited visibility.
-
Ralf Jung authored
Add both non-expansive and contractive functors, and bundle them for the general Iris instance as well as the global functor construction This allows us to move the \later in the user-defined functor to any place we want. In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.
Ralf Jung authoredAdd both non-expansive and contractive functors, and bundle them for the general Iris instance as well as the global functor construction This allows us to move the \later in the user-defined functor to any place we want. In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.