• Robbert Krebbers's avatar
    CMRAs with partial cores. · cfb00b3e
    Robbert Krebbers authored
    Based on an idea and WIP commits of J-H. Jourdan: the core of a CMRA
    A is now a partial function A → option A.
    
    TODO: define sum CMRA
    TODO: remove one shot CMRA and define it in terms of sum
    cfb00b3e
Name
Last commit
Last update
algebra 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...
proofmode Loading commit data...
tests Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
naming.txt Loading commit data...