-
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.
780f6b82