diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | theories/Bool/Bool.v | 26 | ||||
| -rw-r--r-- | theories/Init/Datatypes.v | 36 |
3 files changed, 37 insertions, 26 deletions
@@ -13,6 +13,7 @@ Libraries - Better computational behavior of some constants (eq_nat_dec more efficient, Z_lt_le_dec transparent, ...) [exceptionally source of incompatibilities]. +- Boolean operators moved from module Bool to module Datatypes. Notations diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index d8b900686..1bd56a1ee 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -126,9 +126,8 @@ Proof. destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity. Qed. - (************************) -(** * Logical combinators *) +(** * A synonym of [if] on [bool] *) (************************) Definition ifb (b1 b2 b3:bool) : bool := @@ -137,31 +136,8 @@ Definition ifb (b1 b2 b3:bool) : bool := | false => b3 end. -Definition andb (b1 b2:bool) : bool := ifb b1 b2 false. - -Definition orb (b1 b2:bool) : bool := ifb b1 true b2. - -Definition implb (b1 b2:bool) : bool := ifb b1 b2 true. - -Definition xorb (b1 b2:bool) : bool := - match b1, b2 with - | true, true => false - | true, false => true - | false, true => true - | false, false => false - end. - -Definition negb (b:bool) := if b then false else true. - -Infix "||" := orb (at level 50, left associativity) : bool_scope. -Infix "&&" := andb (at level 40, left associativity) : bool_scope. - Open Scope bool_scope. -Delimit Scope bool_scope with bool. - -Bind Scope bool_scope with bool. - (****************************) (** * De Morgan laws *) (****************************) diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index ab6469ad9..912192b26 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -26,6 +26,35 @@ Inductive bool : Set := Add Printing If bool. +Delimit Scope bool_scope with bool. + +Bind Scope bool_scope with bool. + +(** Basic boolean operators *) + +Definition andb (b1 b2:bool) : bool := if b1 then b2 else false. + +Definition orb (b1 b2:bool) : bool := if b1 then true else b2. + +Definition implb (b1 b2:bool) : bool := if b1 then b2 else true. + +Definition xorb (b1 b2:bool) : bool := + match b1, b2 with + | true, true => false + | true, false => true + | false, true => true + | false, false => false + end. + +Definition negb (b:bool) := if b then false else true. + +Infix "||" := orb (at level 50, left associativity) : bool_scope. +Infix "&&" := andb (at level 40, left associativity) : bool_scope. + +(** Interpretation of booleans as propositions *) + +Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. + (** [nat] is the datatype of natural numbers built from [O] and successor [S]; note that the constructor name is the letter O. Numbers in [nat] can be denoted using a decimal notation; @@ -70,7 +99,7 @@ Definition option_map (A B:Type) (f:A->B) o := end. (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) -(* Syntax defined in Specif.v *) + Inductive sum (A B:Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. @@ -82,6 +111,7 @@ Notation "x + y" := (sum x y) : type_scope. Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. + Add Printing Let prod. Notation "x * y" := (prod x y) : type_scope. @@ -135,6 +165,8 @@ Definition CompOpp (r:comparison) := | Gt => Lt end. +(* begin hide *) + (* Compatibility *) Notation prodT := prod (only parsing). @@ -146,3 +178,5 @@ Notation fstT := fst (only parsing). Notation sndT := snd (only parsing). Notation prodT_uncurry := prod_uncurry (only parsing). Notation prodT_curry := prod_curry (only parsing). + +(* end hide *) |