Skip to content
Snippets Groups Projects
Commit 5f26f6cd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add tests for `set_solver` on `dom`.

parent 8e949e3c
No related branches found
No related tags found
1 merge request!116Add `set_solver` support for `dom`
From stdpp Require Import fin_maps.
From stdpp Require Import fin_maps fin_map_dom.
Section map_disjoint.
Context `{FinMap K M}.
......@@ -11,3 +11,14 @@ Section map_disjoint.
m2 !! i = None m1 ## {[ i := x ]} m2 m2 ## <[i:=x]> m1 m1 !! i = None.
Proof. intros. solve_map_disjoint. Qed.
End map_disjoint.
Section map_dom.
Context `{FinMapDom K M D}.
Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
{[i; j]} dom D (<[i:=x]> (<[j:=y]> ( : M A))).
Proof. set_solver. Qed.
Lemma set_solver_dom_disjoint {A} (X : D) : dom D ( : M A) ## X.
Proof. set_solver. Qed.
End map_dom.
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