diff options
Diffstat (limited to 'theories/Arith/Bool_nat.v')
| -rw-r--r-- | theories/Arith/Bool_nat.v | 36 |
1 files changed, 16 insertions, 20 deletions
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v index f9f6eeb19b..8b1b3a8c20 100644 --- a/theories/Arith/Bool_nat.v +++ b/theories/Arith/Bool_nat.v @@ -10,34 +10,30 @@ Require Export Compare_dec. Require Export Peano_dec. -Require Sumbool. +Require Import Sumbool. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Implicit Variables Type m,n,x,y:nat. +Implicit Types m n x y : nat. (** The decidability of equality and order relations over type [nat] give some boolean functions with the adequate specification. *) -Definition notzerop := [n:nat] (sumbool_not ? ? (zerop n)). -Definition lt_ge_dec : (x,y:nat){(lt x y)}+{(ge x y)} := - [n,m:nat] (sumbool_not ? ? (le_lt_dec m n)). +Definition notzerop n := sumbool_not _ _ (zerop n). +Definition lt_ge_dec : forall x y, {x < y} + {x >= y} := + fun n m => sumbool_not _ _ (le_lt_dec m n). -Definition nat_lt_ge_bool := - [x,y:nat](bool_of_sumbool (lt_ge_dec x y)). -Definition nat_ge_lt_bool := - [x,y:nat](bool_of_sumbool (sumbool_not ? ? (lt_ge_dec x y))). +Definition nat_lt_ge_bool x y := bool_of_sumbool (lt_ge_dec x y). +Definition nat_ge_lt_bool x y := + bool_of_sumbool (sumbool_not _ _ (lt_ge_dec x y)). -Definition nat_le_gt_bool := - [x,y:nat](bool_of_sumbool (le_gt_dec x y)). -Definition nat_gt_le_bool := - [x,y:nat](bool_of_sumbool (sumbool_not ? ? (le_gt_dec x y))). +Definition nat_le_gt_bool x y := bool_of_sumbool (le_gt_dec x y). +Definition nat_gt_le_bool x y := + bool_of_sumbool (sumbool_not _ _ (le_gt_dec x y)). -Definition nat_eq_bool := - [x,y:nat](bool_of_sumbool (eq_nat_dec x y)). -Definition nat_noteq_bool := - [x,y:nat](bool_of_sumbool (sumbool_not ? ? (eq_nat_dec x y))). +Definition nat_eq_bool x y := bool_of_sumbool (eq_nat_dec x y). +Definition nat_noteq_bool x y := + bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)). -Definition zerop_bool := [x:nat](bool_of_sumbool (zerop x)). -Definition notzerop_bool := [x:nat](bool_of_sumbool (notzerop x)). +Definition zerop_bool x := bool_of_sumbool (zerop x). +Definition notzerop_bool x := bool_of_sumbool (notzerop x).
\ No newline at end of file |