diff options
Diffstat (limited to 'theories/Classes/SetoidDec.v')
| -rw-r--r-- | theories/Classes/SetoidDec.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 86a2bef80..26e1ab244 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -54,7 +54,7 @@ Open Local Scope program_scope. (** Invert the branches. *) -Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y). +Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y). (** Overloaded notation for inequality. *) @@ -62,10 +62,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70). (** Define boolean versions, losing the logical information. *) -Definition equiv_decb [ ! EqDec A ] (x y : A) : bool := +Definition equiv_decb [ EqDec A ] (x y : A) : bool := if x == y then true else false. -Definition nequiv_decb [ ! EqDec A ] (x y : A) : bool := +Definition nequiv_decb [ EqDec A ] (x y : A) : bool := negb (equiv_decb x y). Infix "==b" := equiv_decb (no associativity, at level 70). @@ -97,7 +97,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) := reflexivity. Qed. -Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => +Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] => prod_eqdec : EqDec (@eq_setoid (prod A B)) := equiv_dec x y := dest x as (x1, x2) in @@ -113,7 +113,7 @@ Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => Require Import Coq.Program.FunctionalExtensionality. -Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) := +Program Instance [ ! EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) := equiv_dec f g := if f true == g true then if f false == g false then in_left |