ZArith_base, Zbool, Bool_nat

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 0 deletions

diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 817212909..84e74f86b 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -62,3 +62,16 @@ Qed.
 End connectives.
 
 Hints Resolve sumbool_and sumbool_or sumbool_not : core.
+
+
+(** Any decidability function in type [sumbool] can be turned into a function
+    returning a boolean with the corresponding specification: *)
+
+Definition bool_of_sumbool : 
+  (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }.
+Proof.
+Intros A B H.
+Elim H; [ Intro; Exists true; Assumption
+        | Intro; Exists false; Assumption ].
+Save.
+Implicits bool_of_sumbool.