diff options
Diffstat (limited to 'theories/Classes/EquivDec.v')
| -rw-r--r-- | theories/Classes/EquivDec.v | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 4b9b26384..e87482d84 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Decidable equivalences. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud - * 91405 Orsay, France *) +(** * Decidable equivalences. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -18,8 +18,8 @@ Require Export Coq.Classes.Equivalence. -(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more - classically. *) +(** The [DecidableSetoid] class asserts decidability of a [Setoid]. + It can be useful in proofs to reason more classically. *) Require Import Coq.Logic.Decidable. Require Import Coq.Bool.Bool. @@ -31,13 +31,15 @@ Open Scope equiv_scope. Class DecidableEquivalence `(equiv : Equivalence A) := setoid_decidable : forall x y : A, decidable (x === y). -(** The [EqDec] class gives a decision procedure for a particular setoid equality. *) +(** The [EqDec] class gives a decision procedure for a particular + setoid equality. *) Class EqDec A R {equiv : Equivalence R} := equiv_dec : forall x y : A, { x === y } + { x =/= y }. -(** We define the [==] overloaded notation for deciding equality. It does not take precedence - of [==] defined in the type scope, hence we can have both at the same time. *) +(** We define the [==] overloaded notation for deciding equality. It does not + take precedence of [==] defined in the type scope, hence we can have both + at the same time. *) Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope. @@ -70,13 +72,14 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). (** Decidable leibniz equality instances. *) -(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) +(** The equiv is burried inside the setoid, but we can recover it by specifying + which setoid we're talking about. *) Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec. Program Instance bool_eqdec : EqDec bool eq := bool_dec. -Program Instance unit_eqdec : EqDec unit eq := λ x y, in_left. +Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Next Obligation. Proof. @@ -105,8 +108,8 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) : | inl _, inr _ | inr _, inl _ => in_right end }. -(** Objects of function spaces with countable domains like bool have decidable equality. - Proving the reflection requires functional extensionality though. *) +(** Objects of function spaces with countable domains like bool have decidable + equality. Proving the reflection requires functional extensionality though. *) Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := { equiv_dec f g := |