Commit 3c2d317a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add test.

parent b3901a51
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).
......
Supports Markdown
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