From 3c2d317ae3ff6bf0c9fa51ef5bf230f95abd655d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Nov 2021 15:30:07 +0100
Subject: [PATCH] Add test.

---
 tests/proofmode.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 73027cdbd..66cebcc72 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import gmap.
 From iris.bi Require Import laterable.
 From iris.proofmode Require Import tactics intro_patterns.
 From iris.prelude Require Import options.
@@ -81,6 +82,11 @@ Proof.
   auto.
 Qed.
 
+Lemma test_iRewrite_dom `{!BiInternalEq PROP} {A : ofe} (m1 m2 : gmap nat A) :
+  m1 ≡ m2 ⊢@{PROP}
+  ⌜ dom (gset nat) m1 = dom (gset nat) m2 ⌝.
+Proof. iIntros "H". by iRewrite "H". Qed.
+
 Check "test_iDestruct_and_emp".
 Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
   P ∧ emp -∗ emp ∧ Q -∗ <affine> (P ∗ Q).
-- 
GitLab