• Robbert Krebbers's avatar
    Step-indexed order on CMRAs · 58096261
    Robbert Krebbers authored
    * Remove the order from RAs, it is now defined in terms of the ⋅ operation.
    * Define ownership using the step-indexed order.
    * Remove the order also from DRAs and change STS accordingly. While doing
      that, I changed STS to no longer use decidable token sets, which removes the
      requirement of decidable equality on tokens.
    58096261
collections.v 25.7 KB