Commit 60e1e123 authored by Ralf Jung's avatar Ralf Jung
Browse files

provide a way to get bbelow mkSet

parent d436e40c
......@@ -18,6 +18,9 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
Instance set_collection : Collection A (set A).
Proof. by split; [split | |]; repeat intro. Qed.
Lemma mkSet_elem_of {A} (f : A Prop) x : f x x mkSet f.
Proof. done. Qed.
Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
Instance set_bind : MBind set := λ A B (f : A set B) (X : set A),
mkSet (λ b, a, b f a a X).
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