Bool: iff lemmas about or, a reflect inductive, an is_true function

 For the moment, almost no lemmas about (reflect P b), just the proofs
 that it is equivalent with an P<->b=true.

 is_true b is (b=true), and is meant to be added as a coercion
 if one wants it. In the StdLib, this coercion is not globally
 activated, but particular files are free to use Local Coercion...

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

1 files changed, 8 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 782ff6ca9..fcd053e89 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -74,6 +74,14 @@ Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
 Hint Constructors eq_true : eq_true.
 
+(** Another way of interpreting booleans as propositions *)
+
+Definition is_true b := b = true.
+
+(** [is_true] can be activated as a coercion by
+   (Local) Coercion is_true : bool >-> Prop.
+*)
+
 (** Additional rewriting lemmas about [eq_true] *)
 
 Lemma eq_true_ind_r :