Commit f2eabe78 authored by Robbert Krebbers's avatar Robbert Krebbers

Close issue #299: `leibnizO` finds convoluted proof for definitions

parent 79f576aa
From iris.base_logic.lib Require Import invariants.
(** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
with carriers that are definitionally equal. See also
https://gitlab.mpi-sws.org/iris/iris/issues/299 *)
Definition tag := nat.
Canonical Structure tagO := leibnizO tag.
Goal tagO = natO.
Proof. reflexivity. Qed.
Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Section tests.
......
......@@ -885,7 +885,10 @@ Section discrete_ofe.
End discrete_ofe.
Notation discreteO A := (OfeT A (discrete_ofe_mixin _)).
Notation leibnizO A := (OfeT A (@discrete_ofe_mixin _ equivL _)).
(** Force the [Equivalence] proof to be [eq_equivalence] so that it does not
find another one, like [ofe_equivalence], in the case of aliases. See also
https://gitlab.mpi-sws.org/iris/iris/issues/229 *)
Notation leibnizO A := (OfeT A (@discrete_ofe_mixin _ equivL eq_equivalence)).
(** In order to define a discrete CMRA with carrier [A] (in the file [cmra.v])
we need to determine the [Equivalence A] proof that was used to construct the
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment