Skip to content

Make the setoid equivalence and metric for excl and csum independent from the chosen OFE

Jacques-Henri Jourdan requested to merge jh/independent_metric into master

Up to now, these 4 inductives syntactically depend on the OFE, so that we cannot rewrite an equality using (ofe_equiv (cmra_ofe (exclR ....))) if we only have proper instances for (ofe_equiv (exclC ...)).

We can solve this problem by doing these changes. Is there any reason why we did not do that before ?

PS : This branch follows jh/cancellale for convenience (in Lambdarust). I can rebase it on master or anything else if needed.

Merge request reports