Commit ff621c43 authored by Ralf Jung's avatar Ralf Jung

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

parents e767481f 1e489d19
......@@ -20,7 +20,7 @@ Proof. by split; [split | |]; repeat intro. Qed.
Lemma mkSet_elem_of {A} (f : A Prop) x : (x mkSet f) = f x.
Proof. done. Qed.
Lemma mkSet_not_elem_of {A} (f : A Prop) x : (x mkSet f) = (~f x).
Lemma mkSet_not_elem_of {A} (f : A Prop) x : (x mkSet f) = (¬f x).
Proof. done. Qed.
Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
......
Markdown is supported
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