Commit b3901a51 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add `Proper` instance for `Dom` on `gmap`.

parent ff3cf284
From stdpp Require Export list gmap.
From iris.algebra Require Export list cmra.
From iris.algebra Require Import gset.
From iris.algebra Require Import updates local_updates proofmode_classes big_op.
From iris.prelude Require Import options.
......@@ -94,6 +95,9 @@ Lemma insert_idN n m i x :
m !! i {n} Some x <[i:=x]>m {n} m.
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
Global Instance gmap_dom_ne n :
Proper (({n}@{gmap K A}) ==> (=)) (dom (gset K)).
Proof. intros m1 m2 Hm. apply set_eq=> k. by rewrite !elem_of_dom Hm. Qed.
End ofe.
Global Instance map_seq_ne {A : ofe} start :
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