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

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 476491f4 ff621c43
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
theories/sets.v
+ 2
− 2
View file @ a2af977f
...@@ -18,9 +18,9 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2, ...@@ -18,9 +18,9 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
Instance set_collection : Collection A (set A). Instance set_collection : Collection A (set A).
Proof. by split; [split | |]; repeat intro. Qed. Proof. by split; [split | |]; repeat intro. Qed.
Lemma mkSet_elem_of {A} (f : A → Prop) x : f x → x ∈ mkSet f. Lemma mkSet_elem_of {A} (f : A → Prop) x : (x ∈ mkSet f) = f x.
Proof. done. Qed. Proof. done. Qed.
Lemma mkSet_not_elem_of {A} (f : A → Prop) x : ¬f x → x ∉ mkSet f. Lemma mkSet_not_elem_of {A} (f : A → Prop) x : (x ∉ mkSet f) = (¬f x).
Proof. done. Qed. Proof. done. Qed.
Instance set_ret : MRet set := λ A (x : A), {[ x ]}. Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
......
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