diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Classes/Functions.v | 14 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 6 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 2 |
3 files changed, 11 insertions, 11 deletions
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 64eee17d8e..8da1c31762 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop := +Class Injective ((m : Morphism (A -> B) (RA ++> RB) f)) : Prop := injective : forall x y : A, RB (f x) (f y) -> RA x y. -Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop := +Class ((m : Morphism (A -> B) (RA ++> RB) f)) => Surjective : Prop := surjective : forall y, exists x : A, RB y (f x). -Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] := +Definition Bijective ((m : Morphism (A -> B) (RA ++> RB) (f : A -> B))) := Injective m /\ Surjective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism := +Class MonoMorphism (( m : Morphism (A -> B) (eqA ++> eqB) )) := monic :> Injective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := +Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := epic :> Surjective m. -Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := +Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m. -Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism. +Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ ! IsoMorphism m ] => AutoMorphism. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 99eda0ae1b..ddd7b38da4 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -172,11 +172,11 @@ Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 := (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) -Class [ equ : Equivalence A eqA ] => Antisymmetric (R : relation A) := +Class Antisymmetric ((equ : Equivalence A eqA)) (R : relation A) := antisymmetry : forall x y, R x y -> R y x -> eqA x y. -Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] : - Antisymmetric eq (flip R). +Program Instance flip_antiSymmetric {{Antisymmetric A eqA R}} : + ! Antisymmetric A eqA (flip R). (** Leibinz equality [eq] is an equivalence relation. The instance has low priority as it is always applicable diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 07a6985c97..8d40c19a5e 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -32,7 +32,7 @@ Class DecidableSetoid A [ Setoid A ] := (** The [EqDec] class gives a decision procedure for a particular setoid equality. *) -Class [ s : Setoid A ] => EqDec := +Class (( s : Setoid A )) => EqDec := equiv_dec : forall x y : A, { x == y } + { x =/= y }. (** We define the [==] overloaded notation for deciding equality. It does not take precedence |