• Robbert Krebbers's avatar
    No longer use option for local updates. · bee413b8
    Robbert Krebbers authored
    Instead, I separate it into a total function and a predicate
    describe whether the action is allowed or not. This has some
    * It is much easier to deal with total functions and predicates
      in Coq than with functions into option.
    * Already existing functions do not need to be wrapped. Instead,
      when using a local update you end up with a sensible side
      condition as a Coq Prop.
    * The definition of local updates (and all CMRA instances) no
      longer depend on option.
excl.v 7.35 KB