• Ralf Jung's avatar
    Add both non-expansive and contractive functors, and bundle them for the... · 2467bf21
    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.
    2467bf21
Name
Last commit
Last update
algebra Loading commit data...
barrier Loading commit data...
benchmark Loading commit data...
docs Loading commit data...
heap_lang Loading commit data...
prelude Loading commit data...
program_logic Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
README Loading commit data...
_CoqProject Loading commit data...