From 60e1e1234248abfc934b46d57d1e57fe358c80bb Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 16 Feb 2016 11:21:12 +0100 Subject: [PATCH] provide a way to get bbelow mkSet --- prelude/sets.v | 3 +++ 1 file changed, 3 insertions(+) diff --git a/prelude/sets.v b/prelude/sets.v index e92b14e6f..758915bcd 100644 --- a/prelude/sets.v +++ b/prelude/sets.v @@ -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). -- GitLab