Skip to content
Snippets Groups Projects
Verified Commit 76aee980 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Dorian Lesbre
Browse files

Add test for `set_solver` on `img`.

parent 9ac361a5
No related branches found
No related tags found
1 merge request!444Add images (codomains) to finite maps
...@@ -22,3 +22,11 @@ Section map_dom. ...@@ -22,3 +22,11 @@ Section map_dom.
Lemma set_solver_dom_disjoint {A} (X : D) : dom ( : M A) ## X. Lemma set_solver_dom_disjoint {A} (X : D) : dom ( : M A) ## X.
Proof. set_solver. Qed. Proof. set_solver. Qed.
End map_dom. End map_dom.
Section map_img.
Context `{FinMap K M, Set_ A SA}.
Lemma set_solver_map_img i x :
map_img ( : M A) ⊆@{SA} map_img ({[ i := x ]} : M A).
Proof. set_unfold. set_solver. Qed.
End map_img.
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment