Skip to content
Snippets Groups Projects
Commit bd9d16c9 authored by Ralf Jung's avatar Ralf Jung
Browse files

don't test 'Hint Mode Equiv !'; wait for Coq fix instead

parent 366d607e
No related branches found
No related tags found
No related merge requests found
...@@ -2,35 +2,20 @@ From iris.algebra Require Import auth excl lib.gmap_view. ...@@ -2,35 +2,20 @@ From iris.algebra Require Import auth excl lib.gmap_view.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
Section test_dist_equiv_mode. Section test_dist_equiv_mode.
Local Unset Mangle Names.
(* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441. (* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441.
From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *) From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
(* succeeds *)
Lemma list_dist_lookup {A : ofe} n (l1 l2 : list A) : Lemma list_dist_lookup {A : ofe} n (l1 l2 : list A) :
l1 {n} l2 i, l1 !! i {n} l2 !! i. l1 {n} l2 i, l1 !! i {n} l2 !! i.
Abort. Abort.
(* analogous test for [Equiv] and https://github.com/coq/coq/issues/14441. (* analogous test for [Equiv] and https://github.com/coq/coq/issues/14441.
From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *) From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) : Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
l1 l2 i, l1 !! i l2 !! i. l1 l2 i, l1 !! i l2 !! i.
Abort. Abort.
Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) : Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) :
l1 l2 i, l1 !! i l2 !! i. l1 l2 i, l1 !! i l2 !! i.
Abort. Abort.
Local Hint Mode Equiv ! : typeclass_instances.
(* succeeds *)
Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
l1 l2 i, l1 !! i l2 !! i.
Abort.
(* fails due to https://github.com/coq/coq/issues/14441; commented out, hoping
for a fix in Coq. *)
(* Fail Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) :
l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i. *)
End test_dist_equiv_mode. End test_dist_equiv_mode.
(** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs (** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment