diff --git a/tests/algebra.v b/tests/algebra.v index 92c42c4b4f6f9e9071dafaad733c00d9fbd49169..cff006b35fb5dad5262206b75e9b9286d69c142f 100644 --- a/tests/algebra.v +++ b/tests/algebra.v @@ -1,3 +1,4 @@ +From iris.algebra Require Import auth excl. From iris.base_logic.lib Require Import invariants. (** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs @@ -34,3 +35,16 @@ Proof. - apply _. - reflexivity. Qed. + +(** Regression test for <https://gitlab.mpi-sws.org/iris/iris/issues/255>. *) +Definition testR := authR (prodUR + (prodUR + (optionUR (exclR unitO)) + (optionUR (exclR unitO))) + (optionUR (agreeR (boolO)))). +Section test_prod. + Context `{!inG Σ testR}. + Lemma test_prod_persistent γ : + Persistent (PROP:=iPropI Σ) (own γ (◯((None, None), Some (to_agree true)))). + Proof. apply _. Qed. +End test_prod.