diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/countalg.v | 374 | ||||
| -rw-r--r-- | mathcomp/algebra/finalg.v | 464 | ||||
| -rw-r--r-- | mathcomp/algebra/ring_quotient.v | 90 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 340 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 257 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 22 | ||||
| -rw-r--r-- | mathcomp/field/falgebra.v | 44 | ||||
| -rw-r--r-- | mathcomp/field/fieldext.v | 106 | ||||
| -rw-r--r-- | mathcomp/field/finfield.v | 6 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 48 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 8 | ||||
| -rw-r--r-- | mathcomp/ssreflect/choice.v | 28 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 22 | ||||
| -rw-r--r-- | mathcomp/ssreflect/generic_quotient.v | 19 |
15 files changed, 919 insertions, 915 deletions
diff --git a/mathcomp/algebra/countalg.v b/mathcomp/algebra/countalg.v index 21000e4..f82a231 100644 --- a/mathcomp/algebra/countalg.v +++ b/mathcomp/algebra/countalg.v @@ -44,14 +44,14 @@ Variables (type base_type : Type) (class_of base_of : Type -> Type). Variable base_sort : base_type -> Type. (* Explicits *) -Variable Pack : forall T, class_of T -> Type -> type. +Variable Pack : forall T, class_of T -> type. Variable Class : forall T, base_of T -> mixin_of T -> class_of T. Variable base_class : forall bT, base_of (base_sort bT). Definition gen_pack T := fun bT b & phant_id (base_class bT) b => fun fT c m & phant_id (Countable.class fT) (Countable.Class c m) => - Pack (@Class T b m) T. + Pack (@Class T b m). End Generic. @@ -69,20 +69,20 @@ Record class_of M := Local Coercion base : class_of >-> GRing.Zmodule.class_of. Local Coercion mixin : class_of >-> mixin_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.Zmodule.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (cnt_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (cnt_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. -Definition join_countType := @Countable.Pack zmodType (cnt_ xclass) xT. +Definition join_countType := @Countable.Pack zmodType (cnt_ xclass). End ClassDef. @@ -117,22 +117,22 @@ Definition base2 R (c : class_of R) := Zmodule.Class (base c) (mixin c). Local Coercion base : class_of >-> GRing.Ring.class_of. Local Coercion base2 : class_of >-> Zmodule.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.Ring.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (cnt_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass cT. -Definition countZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition join_countType := @Countable.Pack ringType (cnt_ xclass) xT. -Definition join_countZmodType := @Zmodule.Pack ringType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (cnt_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition countZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition join_countType := @Countable.Pack ringType (cnt_ xclass). +Definition join_countZmodType := @Zmodule.Pack ringType xclass. End ClassDef. @@ -173,25 +173,25 @@ Definition base2 R (c : class_of R) := Ring.Class (base c) (mixin c). Local Coercion base : class_of >-> GRing.ComRing.class_of. Local Coercion base2 : class_of >-> Ring.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.ComRing.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (cnt_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition countZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition countRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition join_countType := @Countable.Pack comRingType (cnt_ xclass) xT. -Definition join_countZmodType := @Zmodule.Pack comRingType xclass xT. -Definition join_countRingType := @Ring.Pack comRingType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (cnt_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition countZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition countRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition join_countType := @Countable.Pack comRingType (cnt_ xclass). +Definition join_countZmodType := @Zmodule.Pack comRingType xclass. +Definition join_countRingType := @Ring.Pack comRingType xclass. End ClassDef. @@ -237,26 +237,26 @@ Definition base2 R (c : class_of R) := Ring.Class (base c) (mixin c). Local Coercion base : class_of >-> GRing.UnitRing.class_of. Local Coercion base2 : class_of >-> Ring.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.UnitRing.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (cnt_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition countZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition countRingType := @Ring.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (cnt_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition countZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition countRingType := @Ring.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. -Definition join_countType := @Countable.Pack unitRingType (cnt_ xclass) xT. -Definition join_countZmodType := @Zmodule.Pack unitRingType xclass xT. -Definition join_countRingType := @Ring.Pack unitRingType xclass xT. +Definition join_countType := @Countable.Pack unitRingType (cnt_ xclass). +Definition join_countZmodType := @Zmodule.Pack unitRingType xclass. +Definition join_countRingType := @Ring.Pack unitRingType xclass. End ClassDef. @@ -304,36 +304,36 @@ Local Coercion base : class_of >-> GRing.ComUnitRing.class_of. Local Coercion base2 : class_of >-> ComRing.class_of. Local Coercion base3 : class_of >-> UnitRing.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.ComUnitRing.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (cnt_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition countZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition countRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition countComRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition countUnitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. - -Definition join_countType := @Countable.Pack comUnitRingType (cnt_ xclass) xT. -Definition join_countZmodType := @Zmodule.Pack comUnitRingType xclass xT. -Definition join_countRingType := @Ring.Pack comUnitRingType xclass xT. -Definition join_countComRingType := @ComRing.Pack comUnitRingType xclass xT. -Definition join_countUnitRingType := @UnitRing.Pack comUnitRingType xclass xT. -Definition ujoin_countComRingType := @ComRing.Pack unitRingType xclass xT. -Definition cjoin_countUnitRingType := @UnitRing.Pack comRingType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (cnt_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition countZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition countRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition countComRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition countUnitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. + +Definition join_countType := @Countable.Pack comUnitRingType (cnt_ xclass). +Definition join_countZmodType := @Zmodule.Pack comUnitRingType xclass. +Definition join_countRingType := @Ring.Pack comUnitRingType xclass. +Definition join_countComRingType := @ComRing.Pack comUnitRingType xclass. +Definition join_countUnitRingType := @UnitRing.Pack comUnitRingType xclass. +Definition ujoin_countComRingType := @ComRing.Pack unitRingType xclass. +Definition cjoin_countUnitRingType := @UnitRing.Pack comRingType xclass. Definition ccjoin_countUnitRingType := - @UnitRing.Pack countComRingType xclass xT. + @UnitRing.Pack countComRingType xclass. End ClassDef. @@ -393,35 +393,35 @@ Definition base2 R (c : class_of R) := ComUnitRing.Class (base c) (mixin c). Local Coercion base : class_of >-> GRing.IntegralDomain.class_of. Local Coercion base2 : class_of >-> ComUnitRing.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.IntegralDomain.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (cnt_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition countZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition countRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition countComRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition countUnitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. - -Definition join_countType := @Countable.Pack idomainType (cnt_ xclass) xT. -Definition join_countZmodType := @Zmodule.Pack idomainType xclass xT. -Definition join_countRingType := @Ring.Pack idomainType xclass xT. -Definition join_countUnitRingType := @UnitRing.Pack idomainType xclass xT. -Definition join_countComRingType := @ComRing.Pack idomainType xclass xT. -Definition join_countComUnitRingType := @ComUnitRing.Pack idomainType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (cnt_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition countZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition countRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition countComRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition countUnitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition countComUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. + +Definition join_countType := @Countable.Pack idomainType (cnt_ xclass). +Definition join_countZmodType := @Zmodule.Pack idomainType xclass. +Definition join_countRingType := @Ring.Pack idomainType xclass. +Definition join_countUnitRingType := @UnitRing.Pack idomainType xclass. +Definition join_countComRingType := @ComRing.Pack idomainType xclass. +Definition join_countComUnitRingType := @ComUnitRing.Pack idomainType xclass. End ClassDef. @@ -482,38 +482,38 @@ Definition base2 R (c : class_of R) := IntegralDomain.Class (base c) (mixin c). Local Coercion base : class_of >-> GRing.Field.class_of. Local Coercion base2 : class_of >-> IntegralDomain.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.Field.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (cnt_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition countZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition countRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition countComRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition countUnitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition countIdomainType := @IntegralDomain.Pack cT xclass xT. -Definition fieldType := @GRing.Field.Pack cT xclass xT. - -Definition join_countType := @Countable.Pack fieldType (cnt_ xclass) xT. -Definition join_countZmodType := @Zmodule.Pack fieldType xclass xT. -Definition join_countRingType := @Ring.Pack fieldType xclass xT. -Definition join_countUnitRingType := @UnitRing.Pack fieldType xclass xT. -Definition join_countComRingType := @ComRing.Pack fieldType xclass xT. -Definition join_countComUnitRingType := @ComUnitRing.Pack fieldType xclass xT. -Definition join_countIdomainType := @IntegralDomain.Pack fieldType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (cnt_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition countZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition countRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition countComRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition countUnitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition countComUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition countIdomainType := @IntegralDomain.Pack cT xclass. +Definition fieldType := @GRing.Field.Pack cT xclass. + +Definition join_countType := @Countable.Pack fieldType (cnt_ xclass). +Definition join_countZmodType := @Zmodule.Pack fieldType xclass. +Definition join_countRingType := @Ring.Pack fieldType xclass. +Definition join_countUnitRingType := @UnitRing.Pack fieldType xclass. +Definition join_countComRingType := @ComRing.Pack fieldType xclass. +Definition join_countComUnitRingType := @ComUnitRing.Pack fieldType xclass. +Definition join_countIdomainType := @IntegralDomain.Pack fieldType xclass. End ClassDef. @@ -579,42 +579,42 @@ Definition base2 R (c : class_of R) := Field.Class (base c) (mixin c). Local Coercion base : class_of >-> GRing.DecidableField.class_of. Local Coercion base2 : class_of >-> Field.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.DecidableField.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (cnt_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition countZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition countRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition countComRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition countUnitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition countIdomainType := @IntegralDomain.Pack cT xclass xT. -Definition fieldType := @GRing.Field.Pack cT xclass xT. -Definition countFieldType := @Field.Pack cT xclass xT. -Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT. - -Definition join_countType := @Countable.Pack decFieldType (cnt_ xclass) xT. -Definition join_countZmodType := @Zmodule.Pack decFieldType xclass xT. -Definition join_countRingType := @Ring.Pack decFieldType xclass xT. -Definition join_countUnitRingType := @UnitRing.Pack decFieldType xclass xT. -Definition join_countComRingType := @ComRing.Pack decFieldType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (cnt_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition countZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition countRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition countComRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition countUnitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition countComUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition countIdomainType := @IntegralDomain.Pack cT xclass. +Definition fieldType := @GRing.Field.Pack cT xclass. +Definition countFieldType := @Field.Pack cT xclass. +Definition decFieldType := @GRing.DecidableField.Pack cT xclass. + +Definition join_countType := @Countable.Pack decFieldType (cnt_ xclass). +Definition join_countZmodType := @Zmodule.Pack decFieldType xclass. +Definition join_countRingType := @Ring.Pack decFieldType xclass. +Definition join_countUnitRingType := @UnitRing.Pack decFieldType xclass. +Definition join_countComRingType := @ComRing.Pack decFieldType xclass. Definition join_countComUnitRingType := - @ComUnitRing.Pack decFieldType xclass xT. -Definition join_countIdomainType := @IntegralDomain.Pack decFieldType xclass xT. -Definition join_countFieldType := @Field.Pack decFieldType xclass xT. + @ComUnitRing.Pack decFieldType xclass. +Definition join_countIdomainType := @IntegralDomain.Pack decFieldType xclass. +Definition join_countFieldType := @Field.Pack decFieldType xclass. End ClassDef. @@ -685,47 +685,47 @@ Definition base2 R (c : class_of R) := DecidableField.Class (base c) (mixin c). Local Coercion base : class_of >-> GRing.ClosedField.class_of. Local Coercion base2 : class_of >-> DecidableField.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.ClosedField.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (cnt_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition countZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition countRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition countComRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition countUnitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition countIdomainType := @IntegralDomain.Pack cT xclass xT. -Definition fieldType := @GRing.Field.Pack cT xclass xT. -Definition countFieldType := @Field.Pack cT xclass xT. -Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT. -Definition countDecFieldType := @DecidableField.Pack cT xclass xT. -Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT. - -Definition join_countType := @Countable.Pack closedFieldType (cnt_ xclass) xT. -Definition join_countZmodType := @Zmodule.Pack closedFieldType xclass xT. -Definition join_countRingType := @Ring.Pack closedFieldType xclass xT. -Definition join_countUnitRingType := @UnitRing.Pack closedFieldType xclass xT. -Definition join_countComRingType := @ComRing.Pack closedFieldType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (cnt_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition countZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition countRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition countComRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition countUnitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition countComUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition countIdomainType := @IntegralDomain.Pack cT xclass. +Definition fieldType := @GRing.Field.Pack cT xclass. +Definition countFieldType := @Field.Pack cT xclass. +Definition decFieldType := @GRing.DecidableField.Pack cT xclass. +Definition countDecFieldType := @DecidableField.Pack cT xclass. +Definition closedFieldType := @GRing.ClosedField.Pack cT xclass. + +Definition join_countType := @Countable.Pack closedFieldType (cnt_ xclass). +Definition join_countZmodType := @Zmodule.Pack closedFieldType xclass. +Definition join_countRingType := @Ring.Pack closedFieldType xclass. +Definition join_countUnitRingType := @UnitRing.Pack closedFieldType xclass. +Definition join_countComRingType := @ComRing.Pack closedFieldType xclass. Definition join_countComUnitRingType := - @ComUnitRing.Pack closedFieldType xclass xT. + @ComUnitRing.Pack closedFieldType xclass. Definition join_countIdomainType := - @IntegralDomain.Pack closedFieldType xclass xT. -Definition join_countFieldType := @Field.Pack closedFieldType xclass xT. + @IntegralDomain.Pack closedFieldType xclass. +Definition join_countFieldType := @Field.Pack closedFieldType xclass. Definition join_countDecFieldType := - @DecidableField.Pack closedFieldType xclass xT. + @DecidableField.Pack closedFieldType xclass. End ClassDef. diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index 939cd38..3e28760 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -51,14 +51,14 @@ Variable to_choice : forall T, base_of T -> Choice.class_of T. Variable base_sort : base_type -> Type. (* Explicits *) -Variable Pack : forall T, class_of T -> Type -> type. +Variable Pack : forall T, class_of T -> type. Variable Class : forall T b, mixin_of T (to_choice b) -> class_of T. Variable base_class : forall bT, base_of (base_sort bT). Definition gen_pack T := fun bT b & phant_id (base_class bT) b => fun fT m & phant_id (Finite.class fT) (Finite.Class m) => - Pack (@Class T b m) T. + Pack (@Class T b m). End Generic. @@ -81,21 +81,21 @@ Record class_of M := Local Coercion base : class_of >-> GRing.Zmodule.class_of. Local Coercion mixin : class_of >-> mixin_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.Zmodule.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. -Definition join_finType := @Finite.Pack zmodType (fin_ xclass) xT. +Definition join_finType := @Finite.Pack zmodType (fin_ xclass). Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -167,23 +167,23 @@ Definition base2 R (c : class_of R) := Zmodule.Class (mixin c). Local Coercion base : class_of >-> GRing.Ring.class_of. Local Coercion base2 : class_of >-> Zmodule.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.Ring.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) cT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass cT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition join_finType := @Finite.Pack ringType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack ringType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition join_finType := @Finite.Pack ringType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack ringType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -272,26 +272,26 @@ Definition base2 R (c : class_of R) := Ring.Class (mixin c). Local Coercion base : class_of >-> GRing.ComRing.class_of. Local Coercion base2 : class_of >-> Ring.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.ComRing.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition finRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition join_finType := @Finite.Pack comRingType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack comRingType xclass xT. -Definition join_finRingType := @Ring.Pack comRingType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition finRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition join_finType := @Finite.Pack comRingType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack comRingType xclass. +Definition join_finRingType := @Ring.Pack comRingType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -351,27 +351,27 @@ Definition base2 R (c : class_of R) := Ring.Class (mixin c). Local Coercion base : class_of >-> GRing.UnitRing.class_of. Local Coercion base2 : class_of >-> Ring.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.UnitRing.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition finRingType := @Ring.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition finRingType := @Ring.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. -Definition join_finType := @Finite.Pack unitRingType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack unitRingType xclass xT. -Definition join_finRingType := @Ring.Pack unitRingType xclass xT. +Definition join_finType := @Finite.Pack unitRingType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack unitRingType xclass. +Definition join_finRingType := @Ring.Pack unitRingType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -514,36 +514,36 @@ Local Coercion base : class_of >-> GRing.ComUnitRing.class_of. Local Coercion base2 : class_of >-> ComRing.class_of. Local Coercion base3 : class_of >-> UnitRing.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.ComUnitRing.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition finRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition finComRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition finUnitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. - -Definition join_finType := @Finite.Pack comUnitRingType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack comUnitRingType xclass xT. -Definition join_finRingType := @Ring.Pack comUnitRingType xclass xT. -Definition join_finComRingType := @ComRing.Pack comUnitRingType xclass xT. -Definition join_finUnitRingType := @UnitRing.Pack comUnitRingType xclass xT. -Definition ujoin_finComRingType := @ComRing.Pack unitRingType xclass xT. -Definition cjoin_finUnitRingType := @UnitRing.Pack comRingType xclass xT. -Definition fcjoin_finUnitRingType := @UnitRing.Pack finComRingType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition finRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition finComRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition finUnitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. + +Definition join_finType := @Finite.Pack comUnitRingType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack comUnitRingType xclass. +Definition join_finRingType := @Ring.Pack comUnitRingType xclass. +Definition join_finComRingType := @ComRing.Pack comUnitRingType xclass. +Definition join_finUnitRingType := @UnitRing.Pack comUnitRingType xclass. +Definition ujoin_finComRingType := @ComRing.Pack unitRingType xclass. +Definition cjoin_finUnitRingType := @UnitRing.Pack comRingType xclass. +Definition fcjoin_finUnitRingType := @UnitRing.Pack finComRingType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -619,36 +619,36 @@ Definition base2 R (c : class_of R) := ComUnitRing.Class (mixin c). Local Coercion base : class_of >-> GRing.IntegralDomain.class_of. Local Coercion base2 : class_of >-> ComUnitRing.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.IntegralDomain.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition finRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition finComRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition finUnitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition finComUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. - -Definition join_finType := @Finite.Pack idomainType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack idomainType xclass xT. -Definition join_finRingType := @Ring.Pack idomainType xclass xT. -Definition join_finUnitRingType := @UnitRing.Pack idomainType xclass xT. -Definition join_finComRingType := @ComRing.Pack idomainType xclass xT. -Definition join_finComUnitRingType := @ComUnitRing.Pack idomainType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition finRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition finComRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition finUnitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition finComUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. + +Definition join_finType := @Finite.Pack idomainType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack idomainType xclass. +Definition join_finRingType := @Ring.Pack idomainType xclass. +Definition join_finUnitRingType := @UnitRing.Pack idomainType xclass. +Definition join_finComRingType := @ComRing.Pack idomainType xclass. +Definition join_finComUnitRingType := @ComUnitRing.Pack idomainType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -726,39 +726,39 @@ Definition base2 R (c : class_of R) := IntegralDomain.Class (mixin c). Local Coercion base : class_of >-> GRing.Field.class_of. Local Coercion base2 : class_of >-> IntegralDomain.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Definition pack := gen_pack Pack Class GRing.Field.class. Variable cT : type. -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition finRingType := @Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition finComRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition finUnitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition finComUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition finIdomainType := @IntegralDomain.Pack cT xclass xT. -Definition fieldType := @GRing.Field.Pack cT xclass xT. - -Definition join_finType := @Finite.Pack fieldType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack fieldType xclass xT. -Definition join_finRingType := @Ring.Pack fieldType xclass xT. -Definition join_finUnitRingType := @UnitRing.Pack fieldType xclass xT. -Definition join_finComRingType := @ComRing.Pack fieldType xclass xT. -Definition join_finComUnitRingType := @ComUnitRing.Pack fieldType xclass xT. -Definition join_finIdomainType := @IntegralDomain.Pack fieldType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition finRingType := @Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition finComRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition finUnitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition finComUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition finIdomainType := @IntegralDomain.Pack cT xclass. +Definition fieldType := @GRing.Field.Pack cT xclass. + +Definition join_finType := @Finite.Pack fieldType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack fieldType xclass. +Definition join_finRingType := @Ring.Pack fieldType xclass. +Definition join_finUnitRingType := @UnitRing.Pack fieldType xclass. +Definition join_finComRingType := @ComRing.Pack fieldType xclass. +Definition join_finComUnitRingType := @ComUnitRing.Pack fieldType xclass. +Definition join_finIdomainType := @IntegralDomain.Pack fieldType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -870,17 +870,17 @@ Module DecField. Section Joins. Variable cT : Field.type. -Let xT := let: Field.Pack T _ _ := cT in T. +Let xT := let: Field.Pack T _ := cT in T. Let xclass : Field.class_of xT := Field.class cT. Definition type := Eval hnf in DecFieldType cT (DecidableFieldMixin cT). -Definition finType := @Finite.Pack type (fin_ xclass) xT. -Definition finZmodType := @Zmodule.Pack type xclass xT. -Definition finRingType := @Ring.Pack type xclass xT. -Definition finUnitRingType := @UnitRing.Pack type xclass xT. -Definition finComRingType := @ComRing.Pack type xclass xT. -Definition finComUnitRingType := @ComUnitRing.Pack type xclass xT. -Definition finIdomainType := @IntegralDomain.Pack type xclass xT. +Definition finType := @Finite.Pack type (fin_ xclass). +Definition finZmodType := @Zmodule.Pack type xclass. +Definition finRingType := @Ring.Pack type xclass. +Definition finUnitRingType := @UnitRing.Pack type xclass. +Definition finComRingType := @ComRing.Pack type xclass. +Definition finComUnitRingType := @ComUnitRing.Pack type xclass. +Definition finIdomainType := @IntegralDomain.Pack type xclass. Definition baseFinGroupType := base_group type finZmodType finZmodType. Definition finGroupType := fin_group baseFinGroupType cT. @@ -915,23 +915,23 @@ Definition base2 R (c : class_of R) := Zmodule.Class (mixin c). Local Coercion base : class_of >-> GRing.Lmodule.class_of. Local Coercion base2 : class_of >-> Zmodule.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (cT : type phR). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Definition pack := gen_pack (Pack phR) Class (@GRing.Lmodule.class R phR). -Let xT := let: Pack T _ _ := cT in T. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. -Definition join_finType := @Finite.Pack lmodType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack lmodType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. +Definition join_finType := @Finite.Pack lmodType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack lmodType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -991,33 +991,33 @@ Local Coercion base : class_of >-> GRing.Lalgebra.class_of. Local Coercion base2 : class_of >-> Ring.class_of. Local Coercion base3 : class_of >-> Lmodule.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (cT : type phR). Definition pack := gen_pack (Pack phR) Class (@GRing.Lalgebra.class R phR). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition finRingType := @Ring.Pack cT xclass xT. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. -Definition finLmodType := @Lmodule.Pack R phR cT xclass xT. -Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT. - -Definition join_finType := @Finite.Pack lalgType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack lalgType xclass xT. -Definition join_finLmodType := @Lmodule.Pack R phR lalgType xclass xT. -Definition join_finRingType := @Ring.Pack lalgType xclass xT. -Definition rjoin_finLmodType := @Lmodule.Pack R phR ringType xclass xT. -Definition ljoin_finRingType := @Ring.Pack lmodType xclass xT. -Definition fljoin_finRingType := @Ring.Pack finLmodType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition finRingType := @Ring.Pack cT xclass. +Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. +Definition finLmodType := @Lmodule.Pack R phR cT xclass. +Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass. + +Definition join_finType := @Finite.Pack lalgType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack lalgType xclass. +Definition join_finLmodType := @Lmodule.Pack R phR lalgType xclass. +Definition join_finRingType := @Ring.Pack lalgType xclass. +Definition rjoin_finLmodType := @Lmodule.Pack R phR ringType xclass. +Definition ljoin_finRingType := @Ring.Pack lmodType xclass. +Definition fljoin_finRingType := @Ring.Pack finLmodType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -1090,33 +1090,33 @@ Definition base2 M (c : class_of M) := Lalgebra.Class (mixin c). Local Coercion base : class_of >-> GRing.Algebra.class_of. Local Coercion base2 : class_of >->Lalgebra.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (cT : type phR). Definition pack := gen_pack (Pack phR) Class (@GRing.Algebra.class R phR). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition finRingType := @Ring.Pack cT xclass xT. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. -Definition finLmodType := @Lmodule.Pack R phR cT xclass xT. -Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT. -Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT. -Definition algType := @GRing.Algebra.Pack R phR cT xclass xT. - -Definition join_finType := @Finite.Pack algType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack algType xclass xT. -Definition join_finRingType := @Ring.Pack algType xclass xT. -Definition join_finLmodType := @Lmodule.Pack R phR algType xclass xT. -Definition join_finLalgType := @Lalgebra.Pack R phR algType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition finRingType := @Ring.Pack cT xclass. +Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. +Definition finLmodType := @Lmodule.Pack R phR cT xclass. +Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass. +Definition finLalgType := @Lalgebra.Pack R phR cT xclass. +Definition algType := @GRing.Algebra.Pack R phR cT xclass. + +Definition join_finType := @Finite.Pack algType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack algType xclass. +Definition join_finRingType := @Ring.Pack algType xclass. +Definition join_finLmodType := @Lmodule.Pack R phR algType xclass. +Definition join_finLalgType := @Lalgebra.Pack R phR algType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. @@ -1193,48 +1193,48 @@ Local Coercion base : class_of >-> GRing.UnitAlgebra.class_of. Local Coercion base2 : class_of >-> Algebra.class_of. Local Coercion base3 : class_of >-> UnitRing.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (cT : type phR). Definition pack := gen_pack (Pack phR) Class (@GRing.UnitAlgebra.class R phR). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (fin_ xclass) xT. -Definition finType := @Finite.Pack cT (fin_ xclass) xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition finZmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition finRingType := @Ring.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition finUnitRingType := @UnitRing.Pack cT xclass xT. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. -Definition finLmodType := @Lmodule.Pack R phR cT xclass xT. -Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT. -Definition finLalgType := @Lalgebra.Pack R phR cT xclass xT. -Definition algType := @GRing.Algebra.Pack R phR cT xclass xT. -Definition finAlgType := @Algebra.Pack R phR cT xclass xT. -Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT. - -Definition join_finType := @Finite.Pack unitAlgType (fin_ xclass) xT. -Definition join_finZmodType := @Zmodule.Pack unitAlgType xclass xT. -Definition join_finRingType := @Ring.Pack unitAlgType xclass xT. -Definition join_finUnitRingType := @UnitRing.Pack unitAlgType xclass xT. -Definition join_finLmodType := @Lmodule.Pack R phR unitAlgType xclass xT. -Definition join_finLalgType := @Lalgebra.Pack R phR unitAlgType xclass xT. -Definition join_finAlgType := @Algebra.Pack R phR unitAlgType xclass xT. -Definition ljoin_finUnitRingType := @UnitRing.Pack lmodType xclass xT. -Definition fljoin_finUnitRingType := @UnitRing.Pack finLmodType xclass xT. -Definition njoin_finUnitRingType := @UnitRing.Pack lalgType xclass xT. -Definition fnjoin_finUnitRingType := @UnitRing.Pack finLalgType xclass xT. -Definition ajoin_finUnitRingType := @UnitRing.Pack algType xclass xT. -Definition fajoin_finUnitRingType := @UnitRing.Pack finAlgType xclass xT. -Definition ujoin_finLmodType := @Lmodule.Pack R phR unitRingType xclass xT. -Definition ujoin_finLalgType := @Lalgebra.Pack R phR unitRingType xclass xT. -Definition ujoin_finAlgType := @Algebra.Pack R phR unitRingType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (fin_ xclass). +Definition finType := @Finite.Pack cT (fin_ xclass). +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition finZmodType := @Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition finRingType := @Ring.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition finUnitRingType := @UnitRing.Pack cT xclass. +Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. +Definition finLmodType := @Lmodule.Pack R phR cT xclass. +Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass. +Definition finLalgType := @Lalgebra.Pack R phR cT xclass. +Definition algType := @GRing.Algebra.Pack R phR cT xclass. +Definition finAlgType := @Algebra.Pack R phR cT xclass. +Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass. + +Definition join_finType := @Finite.Pack unitAlgType (fin_ xclass). +Definition join_finZmodType := @Zmodule.Pack unitAlgType xclass. +Definition join_finRingType := @Ring.Pack unitAlgType xclass. +Definition join_finUnitRingType := @UnitRing.Pack unitAlgType xclass. +Definition join_finLmodType := @Lmodule.Pack R phR unitAlgType xclass. +Definition join_finLalgType := @Lalgebra.Pack R phR unitAlgType xclass. +Definition join_finAlgType := @Algebra.Pack R phR unitAlgType xclass. +Definition ljoin_finUnitRingType := @UnitRing.Pack lmodType xclass. +Definition fljoin_finUnitRingType := @UnitRing.Pack finLmodType xclass. +Definition njoin_finUnitRingType := @UnitRing.Pack lalgType xclass. +Definition fnjoin_finUnitRingType := @UnitRing.Pack finLalgType xclass. +Definition ajoin_finUnitRingType := @UnitRing.Pack algType xclass. +Definition fajoin_finUnitRingType := @UnitRing.Pack finAlgType xclass. +Definition ujoin_finLmodType := @Lmodule.Pack R phR unitRingType xclass. +Definition ujoin_finLalgType := @Lalgebra.Pack R phR unitRingType xclass. +Definition ujoin_finAlgType := @Algebra.Pack R phR unitRingType xclass. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v index 8745049..7e708ca 100644 --- a/mathcomp/algebra/ring_quotient.v +++ b/mathcomp/algebra/ring_quotient.v @@ -110,11 +110,11 @@ Variables (zeroT : T) (oppT : T -> T) (addT : T -> T -> T). Record zmod_quot_mixin_of (Q : Type) (qc : quot_class_of T Q) (zc : GRing.Zmodule.class_of Q) := ZmodQuotMixinPack { zmod_eq_quot_mixin :> eq_quot_mixin_of eqT qc zc; - _ : \pi_(QuotTypePack qc Q) zeroT = 0 :> GRing.Zmodule.Pack zc Q; - _ : {morph \pi_(QuotTypePack qc Q) : x / - oppT x >-> @GRing.opp (GRing.Zmodule.Pack zc Q) x}; - _ : {morph \pi_(QuotTypePack qc Q) : x y / - addT x y >-> @GRing.add (GRing.Zmodule.Pack zc Q) x y} + _ : \pi_(QuotTypePack qc) zeroT = 0 :> GRing.Zmodule.Pack zc; + _ : {morph \pi_(QuotTypePack qc) : x / + oppT x >-> @GRing.opp (GRing.Zmodule.Pack zc) x}; + _ : {morph \pi_(QuotTypePack qc) : x y / + addT x y >-> @GRing.add (GRing.Zmodule.Pack zc) x y} }. Record zmod_quot_class_of (Q : Type) : Type := ZmodQuotClass { @@ -127,25 +127,25 @@ Record zmod_quot_class_of (Q : Type) : Type := ZmodQuotClass { Structure zmodQuotType : Type := ZmodQuotTypePack { zmod_quot_sort :> Type; _ : zmod_quot_class_of zmod_quot_sort; - _ : Type + }. Implicit Type zqT : zmodQuotType. Definition zmod_quot_class zqT : zmod_quot_class_of zqT := - let: ZmodQuotTypePack _ cT _ as qT' := zqT return zmod_quot_class_of qT' in cT. + let: ZmodQuotTypePack _ cT as qT' := zqT return zmod_quot_class_of qT' in cT. Definition zmod_eq_quot_class zqT (zqc : zmod_quot_class_of zqT) : eq_quot_class_of eqT zqT := EqQuotClass zqc. -Canonical zmodQuotType_eqType zqT := Equality.Pack (zmod_quot_class zqT) zqT. +Canonical zmodQuotType_eqType zqT := Equality.Pack (zmod_quot_class zqT). Canonical zmodQuotType_choiceType zqT := - Choice.Pack (zmod_quot_class zqT) zqT. + Choice.Pack (zmod_quot_class zqT). Canonical zmodQuotType_zmodType zqT := - GRing.Zmodule.Pack (zmod_quot_class zqT) zqT. -Canonical zmodQuotType_quotType zqT := QuotTypePack (zmod_quot_class zqT) zqT. + GRing.Zmodule.Pack (zmod_quot_class zqT). +Canonical zmodQuotType_quotType zqT := QuotTypePack (zmod_quot_class zqT). Canonical zmodQuotType_eqQuotType zqT := EqQuotTypePack - (zmod_eq_quot_class (zmod_quot_class zqT)) zqT. + (zmod_eq_quot_class (zmod_quot_class zqT)). Coercion zmodQuotType_eqType : zmodQuotType >-> eqType. Coercion zmodQuotType_choiceType : zmodQuotType >-> choiceType. @@ -156,7 +156,7 @@ Coercion zmodQuotType_eqQuotType : zmodQuotType >-> eqQuotType. Definition ZmodQuotType_pack Q := fun (qT : quotType T) (zT : zmodType) qc zc of phant_id (quot_class qT) qc & phant_id (GRing.Zmodule.class zT) zc => - fun m => ZmodQuotTypePack (@ZmodQuotClass Q qc zc m) Q. + fun m => ZmodQuotTypePack (@ZmodQuotClass Q qc zc m). Definition ZmodQuotMixin_pack Q := fun (qT : eqQuotType eqT) (qc : eq_quot_class_of eqT Q) @@ -165,7 +165,7 @@ Definition ZmodQuotMixin_pack Q := fun e m0 mN mD => @ZmodQuotMixinPack Q qc zc e m0 mN mD. Definition ZmodQuotType_clone (Q : Type) qT cT - of phant_id (zmod_quot_class qT) cT := @ZmodQuotTypePack Q cT Q. + of phant_id (zmod_quot_class qT) cT := @ZmodQuotTypePack Q cT. Lemma zmod_quot_mixinP zqT : zmod_quot_mixin_of (zmod_quot_class zqT) (zmod_quot_class zqT). @@ -216,9 +216,9 @@ Variables (oneT : T) (mulT : T -> T -> T). Record ring_quot_mixin_of (Q : Type) (qc : quot_class_of T Q) (rc : GRing.Ring.class_of Q) := RingQuotMixinPack { ring_zmod_quot_mixin :> zmod_quot_mixin_of eqT zeroT oppT addT qc rc; - _ : \pi_(QuotTypePack qc Q) oneT = 1 :> GRing.Ring.Pack rc Q; - _ : {morph \pi_(QuotTypePack qc Q) : x y / - mulT x y >-> @GRing.mul (GRing.Ring.Pack rc Q) x y} + _ : \pi_(QuotTypePack qc) oneT = 1 :> GRing.Ring.Pack rc; + _ : {morph \pi_(QuotTypePack qc) : x y / + mulT x y >-> @GRing.mul (GRing.Ring.Pack rc) x y} }. Record ring_quot_class_of (Q : Type) : Type := RingQuotClass { @@ -231,30 +231,30 @@ Record ring_quot_class_of (Q : Type) : Type := RingQuotClass { Structure ringQuotType : Type := RingQuotTypePack { ring_quot_sort :> Type; _ : ring_quot_class_of ring_quot_sort; - _ : Type + }. Implicit Type rqT : ringQuotType. Definition ring_quot_class rqT : ring_quot_class_of rqT := - let: RingQuotTypePack _ cT _ as qT' := rqT return ring_quot_class_of qT' in cT. + let: RingQuotTypePack _ cT as qT' := rqT return ring_quot_class_of qT' in cT. Definition ring_zmod_quot_class rqT (rqc : ring_quot_class_of rqT) : zmod_quot_class_of eqT zeroT oppT addT rqT := ZmodQuotClass rqc. Definition ring_eq_quot_class rqT (rqc : ring_quot_class_of rqT) : eq_quot_class_of eqT rqT := EqQuotClass rqc. -Canonical ringQuotType_eqType rqT := Equality.Pack (ring_quot_class rqT) rqT. -Canonical ringQuotType_choiceType rqT := Choice.Pack (ring_quot_class rqT) rqT. +Canonical ringQuotType_eqType rqT := Equality.Pack (ring_quot_class rqT). +Canonical ringQuotType_choiceType rqT := Choice.Pack (ring_quot_class rqT). Canonical ringQuotType_zmodType rqT := - GRing.Zmodule.Pack (ring_quot_class rqT) rqT. + GRing.Zmodule.Pack (ring_quot_class rqT). Canonical ringQuotType_ringType rqT := - GRing.Ring.Pack (ring_quot_class rqT) rqT. -Canonical ringQuotType_quotType rqT := QuotTypePack (ring_quot_class rqT) rqT. + GRing.Ring.Pack (ring_quot_class rqT). +Canonical ringQuotType_quotType rqT := QuotTypePack (ring_quot_class rqT). Canonical ringQuotType_eqQuotType rqT := - EqQuotTypePack (ring_eq_quot_class (ring_quot_class rqT)) rqT. + EqQuotTypePack (ring_eq_quot_class (ring_quot_class rqT)). Canonical ringQuotType_zmodQuotType rqT := - ZmodQuotTypePack (ring_zmod_quot_class (ring_quot_class rqT)) rqT. + ZmodQuotTypePack (ring_zmod_quot_class (ring_quot_class rqT)). Coercion ringQuotType_eqType : ringQuotType >-> eqType. Coercion ringQuotType_choiceType : ringQuotType >-> choiceType. @@ -267,7 +267,7 @@ Coercion ringQuotType_zmodQuotType : ringQuotType >-> zmodQuotType. Definition RingQuotType_pack Q := fun (qT : quotType T) (zT : ringType) qc rc of phant_id (quot_class qT) qc & phant_id (GRing.Ring.class zT) rc => - fun m => RingQuotTypePack (@RingQuotClass Q qc rc m) Q. + fun m => RingQuotTypePack (@RingQuotClass Q qc rc m). Definition RingQuotMixin_pack Q := fun (qT : zmodQuotType eqT zeroT oppT addT) => @@ -277,7 +277,7 @@ Definition RingQuotMixin_pack Q := fun mZ m1 mM => @RingQuotMixinPack Q qc rc mZ m1 mM. Definition RingQuotType_clone (Q : Type) qT cT - of phant_id (ring_quot_class qT) cT := @RingQuotTypePack Q cT Q. + of phant_id (ring_quot_class qT) cT := @RingQuotTypePack Q cT. Lemma ring_quot_mixinP rqT : ring_quot_mixin_of (ring_quot_class rqT) (ring_quot_class rqT). @@ -327,10 +327,10 @@ Record unit_ring_quot_mixin_of (Q : Type) (qc : quot_class_of T Q) (rc : GRing.UnitRing.class_of Q) := UnitRingQuotMixinPack { unit_ring_zmod_quot_mixin :> ring_quot_mixin_of eqT zeroT oppT addT oneT mulT qc rc; - _ : {mono \pi_(QuotTypePack qc Q) : x / - unitT x >-> x \in @GRing.unit (GRing.UnitRing.Pack rc Q)}; - _ : {morph \pi_(QuotTypePack qc Q) : x / - invT x >-> @GRing.inv (GRing.UnitRing.Pack rc Q) x} + _ : {mono \pi_(QuotTypePack qc) : x / + unitT x >-> x \in @GRing.unit (GRing.UnitRing.Pack rc)}; + _ : {morph \pi_(QuotTypePack qc) : x / + invT x >-> @GRing.inv (GRing.UnitRing.Pack rc) x} }. Record unit_ring_quot_class_of (Q : Type) : Type := UnitRingQuotClass { @@ -343,13 +343,13 @@ Record unit_ring_quot_class_of (Q : Type) : Type := UnitRingQuotClass { Structure unitRingQuotType : Type := UnitRingQuotTypePack { unit_ring_quot_sort :> Type; _ : unit_ring_quot_class_of unit_ring_quot_sort; - _ : Type + }. Implicit Type rqT : unitRingQuotType. Definition unit_ring_quot_class rqT : unit_ring_quot_class_of rqT := - let: UnitRingQuotTypePack _ cT _ as qT' := rqT + let: UnitRingQuotTypePack _ cT as qT' := rqT return unit_ring_quot_class_of qT' in cT. Definition unit_ring_ring_quot_class rqT (rqc : unit_ring_quot_class_of rqT) : @@ -360,23 +360,23 @@ Definition unit_ring_eq_quot_class rqT (rqc : unit_ring_quot_class_of rqT) : eq_quot_class_of eqT rqT := EqQuotClass rqc. Canonical unitRingQuotType_eqType rqT := - Equality.Pack (unit_ring_quot_class rqT) rqT. + Equality.Pack (unit_ring_quot_class rqT). Canonical unitRingQuotType_choiceType rqT := - Choice.Pack (unit_ring_quot_class rqT) rqT. + Choice.Pack (unit_ring_quot_class rqT). Canonical unitRingQuotType_zmodType rqT := - GRing.Zmodule.Pack (unit_ring_quot_class rqT) rqT. + GRing.Zmodule.Pack (unit_ring_quot_class rqT). Canonical unitRingQuotType_ringType rqT := - GRing.Ring.Pack (unit_ring_quot_class rqT) rqT. + GRing.Ring.Pack (unit_ring_quot_class rqT). Canonical unitRingQuotType_unitRingType rqT := - GRing.UnitRing.Pack (unit_ring_quot_class rqT) rqT. + GRing.UnitRing.Pack (unit_ring_quot_class rqT). Canonical unitRingQuotType_quotType rqT := - QuotTypePack (unit_ring_quot_class rqT) rqT. + QuotTypePack (unit_ring_quot_class rqT). Canonical unitRingQuotType_eqQuotType rqT := - EqQuotTypePack (unit_ring_eq_quot_class (unit_ring_quot_class rqT)) rqT. + EqQuotTypePack (unit_ring_eq_quot_class (unit_ring_quot_class rqT)). Canonical unitRingQuotType_zmodQuotType rqT := - ZmodQuotTypePack (unit_ring_zmod_quot_class (unit_ring_quot_class rqT)) rqT. + ZmodQuotTypePack (unit_ring_zmod_quot_class (unit_ring_quot_class rqT)). Canonical unitRingQuotType_ringQuotType rqT := - RingQuotTypePack (unit_ring_ring_quot_class (unit_ring_quot_class rqT)) rqT. + RingQuotTypePack (unit_ring_ring_quot_class (unit_ring_quot_class rqT)). Coercion unitRingQuotType_eqType : unitRingQuotType >-> eqType. Coercion unitRingQuotType_choiceType : unitRingQuotType >-> choiceType. @@ -391,7 +391,7 @@ Coercion unitRingQuotType_ringQuotType : unitRingQuotType >-> ringQuotType. Definition UnitRingQuotType_pack Q := fun (qT : quotType T) (rT : unitRingType) qc rc of phant_id (quot_class qT) qc & phant_id (GRing.UnitRing.class rT) rc => - fun m => UnitRingQuotTypePack (@UnitRingQuotClass Q qc rc m) Q. + fun m => UnitRingQuotTypePack (@UnitRingQuotClass Q qc rc m). Definition UnitRingQuotMixin_pack Q := fun (qT : ringQuotType eqT zeroT oppT addT oneT mulT) => @@ -401,7 +401,7 @@ Definition UnitRingQuotMixin_pack Q := fun mR mU mV => @UnitRingQuotMixinPack Q qc rc mR mU mV. Definition UnitRingQuotType_clone (Q : Type) qT cT - of phant_id (unit_ring_quot_class qT) cT := @UnitRingQuotTypePack Q cT Q. + of phant_id (unit_ring_quot_class qT) cT := @UnitRingQuotTypePack Q cT. Lemma unit_ring_quot_mixinP rqT : unit_ring_quot_mixin_of (unit_ring_quot_class rqT) (unit_ring_quot_class rqT). diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 6df490d..5542959 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -626,19 +626,19 @@ Section ClassDef. Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }. Local Coercion base : class_of >-> Choice.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack m := - fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T. + fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. End ClassDef. @@ -892,33 +892,32 @@ Record mixin_of (R : zmodType) : Type := Mixin { Definition EtaMixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 := let _ := @Mixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 in - @Mixin (Zmodule.Pack (Zmodule.class R) R) _ _ + @Mixin (Zmodule.Pack (Zmodule.class R)) _ _ mulA mul1x mulx1 mul_addl mul_addr nz1. Section ClassDef. Record class_of (R : Type) : Type := Class { base : Zmodule.class_of R; - mixin : mixin_of (Zmodule.Pack base R) + mixin : mixin_of (Zmodule.Pack base) }. Local Coercion base : class_of >-> Zmodule.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). - -Definition pack b0 (m0 : mixin_of (@Zmodule.Pack T b0 T)) := +Definition pack b0 (m0 : mixin_of (@Zmodule.Pack T b0)) := fun bT b & phant_id (Zmodule.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. + fun m & phant_id m0 m => Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. End ClassDef. @@ -1504,26 +1503,25 @@ Variable R : ringType. Structure class_of V := Class { base : Zmodule.class_of V; - mixin : mixin_of R (Zmodule.Pack base V) + mixin : mixin_of R (Zmodule.Pack base) }. Local Coercion base : class_of >-> Zmodule.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (phR : phant R) (T : Type) (cT : type phR). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack phR T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack phR T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). - -Definition pack b0 (m0 : mixin_of R (@Zmodule.Pack T b0 T)) := +Definition pack b0 (m0 : mixin_of R (@Zmodule.Pack T b0)) := fun bT b & phant_id (Zmodule.class bT) b => - fun m & phant_id m0 m => Pack phR (@Class T b m) T. + fun m & phant_id m0 m => Pack phR (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. End ClassDef. @@ -1660,33 +1658,33 @@ Variable R : ringType. Record class_of (T : Type) : Type := Class { base : Ring.class_of T; - mixin : Lmodule.mixin_of R (Zmodule.Pack base T); - ext : @axiom R (Lmodule.Pack _ (Lmodule.Class mixin) T) (Ring.mul base) + mixin : Lmodule.mixin_of R (Zmodule.Pack base); + ext : @axiom R (Lmodule.Pack _ (Lmodule.Class mixin)) (Ring.mul base) }. Definition base2 R m := Lmodule.Class (@mixin R m). Local Coercion base : class_of >-> Ring.class_of. Local Coercion base2 : class_of >-> Lmodule.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (phR : phant R) (T : Type) (cT : type phR). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack phR T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack phR T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack T b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0 T) mul0) := +Definition pack T b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0) mul0) := fun bT b & phant_id (Ring.class bT) (b : Ring.class_of T) => fun mT m & phant_id (@Lmodule.class R phR mT) (@Lmodule.Class R T b m) => fun ax & phant_id axT ax => - Pack (Phant R) (@Class T b m ax) T. + Pack (Phant R) (@Class T b m ax). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition lmodType := @Lmodule.Pack R phR cT xclass xT. -Definition lmod_ringType := @Lmodule.Pack R phR ringType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition lmodType := @Lmodule.Pack R phR cT xclass. +Definition lmod_ringType := @Lmodule.Pack R phR ringType xclass. End ClassDef. @@ -2472,22 +2470,22 @@ Record class_of R := Class {base : Ring.class_of R; mixin : commutative (Ring.mul base)}. Local Coercion base : class_of >-> Ring.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack mul0 (m0 : @commutative T T mul0) := fun bT b & phant_id (Ring.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. + fun m & phant_id m0 m => Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. End ClassDef. @@ -2630,28 +2628,28 @@ Variable R : ringType. Record class_of (T : Type) : Type := Class { base : Lalgebra.class_of R T; - mixin : axiom (Lalgebra.Pack _ base T) + mixin : axiom (Lalgebra.Pack _ base) }. Local Coercion base : class_of >-> Lalgebra.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (phR : phant R) (T : Type) (cT : type phR). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack phR T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack phR T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack b0 (ax0 : @axiom R b0) := fun bT b & phant_id (@Lalgebra.class R phR bT) b => - fun ax & phant_id ax0 ax => Pack phR (@Class T b ax) T. + fun ax & phant_id ax0 ax => Pack phR (@Class T b ax). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition lmodType := @Lmodule.Pack R phR cT xclass xT. -Definition lalgType := @Lalgebra.Pack R phR cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition lmodType := @Lmodule.Pack R phR cT xclass. +Definition lalgType := @Lalgebra.Pack R phR cT xclass. End ClassDef. @@ -2744,32 +2742,32 @@ Record mixin_of (R : ringType) : Type := Mixin { Definition EtaMixin R unit inv mulVr mulrV unitP inv_out := let _ := @Mixin R unit inv mulVr mulrV unitP inv_out in - @Mixin (Ring.Pack (Ring.class R) R) unit inv mulVr mulrV unitP inv_out. + @Mixin (Ring.Pack (Ring.class R)) unit inv mulVr mulrV unitP inv_out. Section ClassDef. Record class_of (R : Type) : Type := Class { base : Ring.class_of R; - mixin : mixin_of (Ring.Pack base R) + mixin : mixin_of (Ring.Pack base) }. Local Coercion base : class_of >-> Ring.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack b0 (m0 : mixin_of (@Ring.Pack T b0 T)) := +Definition pack b0 (m0 : mixin_of (@Ring.Pack T b0)) := fun bT b & phant_id (Ring.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. + fun m & phant_id m0 m => Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. End ClassDef. @@ -3078,31 +3076,31 @@ Section ClassDef. Record class_of (R : Type) : Type := Class { base : ComRing.class_of R; - mixin : UnitRing.mixin_of (Ring.Pack base R) + mixin : UnitRing.mixin_of (Ring.Pack base) }. Local Coercion base : class_of >-> ComRing.class_of. Definition base2 R m := UnitRing.Class (@mixin R m). Local Coercion base2 : class_of >-> UnitRing.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (ComRing.class bT) (b : ComRing.class_of T) => fun mT m & phant_id (UnitRing.class mT) (@UnitRing.Class T b m) => - Pack (@Class T b m) T. + Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition comRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @UnitRing.Pack cT xclass xT. -Definition com_unitRingType := @UnitRing.Pack comRingType xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition comRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @UnitRing.Pack cT xclass. +Definition com_unitRingType := @UnitRing.Pack comRingType xclass. End ClassDef. @@ -3142,35 +3140,35 @@ Variable R : ringType. Record class_of (T : Type) : Type := Class { base : Algebra.class_of R T; - mixin : GRing.UnitRing.mixin_of (Ring.Pack base T) + mixin : GRing.UnitRing.mixin_of (Ring.Pack base) }. Definition base2 R m := UnitRing.Class (@mixin R m). Local Coercion base : class_of >-> Algebra.class_of. Local Coercion base2 : class_of >-> UnitRing.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (phR : phant R) (T : Type) (cT : type phR). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@Algebra.class R phR bT) (b : Algebra.class_of R T) => fun mT m & phant_id (UnitRing.mixin (UnitRing.class mT)) m => - Pack (Phant R) (@Class T b m) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition unitRingType := @UnitRing.Pack cT xclass xT. -Definition lmodType := @Lmodule.Pack R phR cT xclass xT. -Definition lalgType := @Lalgebra.Pack R phR cT xclass xT. -Definition algType := @Algebra.Pack R phR cT xclass xT. -Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType xclass xT. -Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType xclass xT. -Definition alg_unitRingType := @Algebra.Pack R phR unitRingType xclass xT. + Pack (Phant R) (@Class T b m). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition unitRingType := @UnitRing.Pack cT xclass. +Definition lmodType := @Lmodule.Pack R phR cT xclass. +Definition lalgType := @Lalgebra.Pack R phR cT xclass. +Definition algType := @Algebra.Pack R phR cT xclass. +Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType xclass. +Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType xclass. +Definition alg_unitRingType := @Algebra.Pack R phR unitRingType xclass. End ClassDef. @@ -4351,28 +4349,28 @@ Definition axiom (R : ringType) := Section ClassDef. Record class_of (R : Type) : Type := - Class {base : ComUnitRing.class_of R; mixin : axiom (Ring.Pack base R)}. + Class {base : ComUnitRing.class_of R; mixin : axiom (Ring.Pack base)}. Local Coercion base : class_of >-> ComUnitRing.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) := +Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) := fun bT b & phant_id (ComUnitRing.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. + fun m & phant_id m0 m => Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition comRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition comRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @ComUnitRing.Pack cT xclass. End ClassDef. @@ -4569,30 +4567,30 @@ Section ClassDef. Record class_of (F : Type) : Type := Class { base : IntegralDomain.class_of F; - mixin : mixin_of (UnitRing.Pack base F) + mixin : mixin_of (UnitRing.Pack base) }. Local Coercion base : class_of >-> IntegralDomain.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) := +Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0)) := fun bT b & phant_id (IntegralDomain.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. + fun m & phant_id m0 m => Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition comRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @IntegralDomain.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition comRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @IntegralDomain.Pack cT xclass. End ClassDef. @@ -4826,30 +4824,30 @@ Record mixin_of (R : unitRingType) : Type := Section ClassDef. Record class_of (F : Type) : Type := - Class {base : Field.class_of F; mixin : mixin_of (UnitRing.Pack base F)}. + Class {base : Field.class_of F; mixin : mixin_of (UnitRing.Pack base)}. Local Coercion base : class_of >-> Field.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) := +Definition pack b0 (m0 : mixin_of (@UnitRing.Pack T b0)) := fun bT b & phant_id (Field.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition comRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @IntegralDomain.Pack cT xclass xT. -Definition fieldType := @Field.Pack cT xclass xT. + fun m & phant_id m0 m => Pack (@Class T b m). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition comRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @IntegralDomain.Pack cT xclass. +Definition fieldType := @Field.Pack cT xclass. End ClassDef. @@ -5068,34 +5066,34 @@ Definition axiom (R : ringType) := Section ClassDef. Record class_of (F : Type) : Type := - Class {base : DecidableField.class_of F; _ : axiom (Ring.Pack base F)}. + Class {base : DecidableField.class_of F; _ : axiom (Ring.Pack base)}. Local Coercion base : class_of >-> DecidableField.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition pack b0 (m0 : axiom (@Ring.Pack T b0 T)) := +Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) := fun bT b & phant_id (DecidableField.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. + fun m & phant_id m0 m => Pack (@Class T b m). (* There should eventually be a constructor from polynomial resolution *) (* that builds the DecidableField mixin using QE. *) -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition comRingType := @ComRing.Pack cT xclass xT. -Definition unitRingType := @UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @IntegralDomain.Pack cT xclass xT. -Definition fieldType := @Field.Pack cT xclass xT. -Definition decFieldType := @DecidableField.Pack cT class xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition comRingType := @ComRing.Pack cT xclass. +Definition unitRingType := @UnitRing.Pack cT xclass. +Definition comUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @IntegralDomain.Pack cT xclass. +Definition fieldType := @Field.Pack cT xclass. +Definition decFieldType := @DecidableField.Pack cT class. End ClassDef. @@ -5183,7 +5181,7 @@ Variables (ringS : subringPred S) (kS : keyed_pred ringS). Definition cast_zmodType (V : zmodType) T (VeqT : V = T :> Type) := let cast mV := let: erefl in _ = T := VeqT return Zmodule.class_of T in mV in - Zmodule.Pack (cast (Zmodule.class V)) T. + Zmodule.Pack (cast (Zmodule.class V)). Variable (T : subType (mem kS)) (V : zmodType) (VeqT: V = T :> Type). @@ -5266,7 +5264,7 @@ Section UnitRing. Definition cast_ringType (Q : ringType) T (QeqT : Q = T :> Type) := let cast rQ := let: erefl in _ = T := QeqT return Ring.class_of T in rQ in - Ring.Pack (cast (Ring.class Q)) T. + Ring.Pack (cast (Ring.class Q)). Variables (R : unitRingType) (S : predPredType R). Variables (ringS : divringPred S) (kS : keyed_pred ringS). diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 5c6f098..ae0c00b 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -163,7 +163,7 @@ Record mixin_of (R : ringType) := Mixin { _ : forall x y, (lt_op x y) = (y != x) && (le_op x y) }. -Local Notation ring_for T b := (@GRing.Ring.Pack T b T). +Local Notation ring_for T b := (@GRing.Ring.Pack T b). (* Base interface. *) Module NumDomain. @@ -175,25 +175,26 @@ Record class_of T := Class { mixin : mixin_of (ring_for T base) }. Local Coercion base : class_of >-> GRing.IntegralDomain.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition clone c of phant_id class c := @Pack T c T. + +Definition clone c of phant_id class c := @Pack T c. Definition pack b0 (m0 : mixin_of (ring_for T b0)) := fun bT b & phant_id (GRing.IntegralDomain.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. + fun m & phant_id m0 m => Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. End ClassDef. @@ -345,7 +346,7 @@ Definition real_closed_axiom : Prop := End ExtensionAxioms. -Local Notation num_for T b := (@NumDomain.Pack T b T). +Local Notation num_for T b := (@NumDomain.Pack T b). (* The rest of the numbers interface hierarchy. *) Module NumField. @@ -358,28 +359,29 @@ Definition base2 R (c : class_of R) := NumDomain.Class (mixin c). Local Coercion base : class_of >-> GRing.Field.class_of. Local Coercion base2 : class_of >-> NumDomain.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). + Definition pack := fun bT b & phant_id (GRing.Field.class bT) (b : GRing.Field.class_of T) => fun mT m & phant_id (NumDomain.class mT) (@NumDomain.Class T b m) => - Pack (@Class T b m) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition numDomainType := @NumDomain.Pack cT xclass xT. -Definition fieldType := @GRing.Field.Pack cT xclass xT. -Definition join_numDomainType := @NumDomain.Pack fieldType xclass xT. + Pack (@Class T b m). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition numDomainType := @NumDomain.Pack cT xclass. +Definition fieldType := @GRing.Field.Pack cT xclass. +Definition join_numDomainType := @NumDomain.Pack fieldType xclass. End ClassDef. @@ -436,36 +438,37 @@ Definition base2 R (c : class_of R) := NumField.Class (mixin c). Local Coercion base : class_of >-> GRing.ClosedField.class_of. Local Coercion base2 : class_of >-> NumField.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). + Definition pack := fun bT b & phant_id (GRing.ClosedField.class bT) (b : GRing.ClosedField.class_of T) => fun mT m & phant_id (NumField.class mT) (@NumField.Class T b m) => - fun mc => Pack (@Class T b m mc) T. -Definition clone := fun b & phant_id class (b : class_of T) => Pack b T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition numDomainType := @NumDomain.Pack cT xclass xT. -Definition fieldType := @GRing.Field.Pack cT xclass xT. -Definition numFieldType := @NumField.Pack cT xclass xT. -Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT. -Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT. -Definition join_dec_numDomainType := @NumDomain.Pack decFieldType xclass xT. -Definition join_dec_numFieldType := @NumField.Pack decFieldType xclass xT. -Definition join_numDomainType := @NumDomain.Pack closedFieldType xclass xT. -Definition join_numFieldType := @NumField.Pack closedFieldType xclass xT. + fun mc => Pack (@Class T b m mc). +Definition clone := fun b & phant_id class (b : class_of T) => Pack b. + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition numDomainType := @NumDomain.Pack cT xclass. +Definition fieldType := @GRing.Field.Pack cT xclass. +Definition numFieldType := @NumField.Pack cT xclass. +Definition decFieldType := @GRing.DecidableField.Pack cT xclass. +Definition closedFieldType := @GRing.ClosedField.Pack cT xclass. +Definition join_dec_numDomainType := @NumDomain.Pack decFieldType xclass. +Definition join_dec_numFieldType := @NumField.Pack decFieldType xclass. +Definition join_numDomainType := @NumDomain.Pack closedFieldType xclass. +Definition join_numFieldType := @NumField.Pack closedFieldType xclass. End ClassDef. @@ -524,26 +527,27 @@ Record class_of R := Class {base : NumDomain.class_of R; _ : @real_axiom (num_for R base)}. Local Coercion base : class_of >-> NumDomain.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition clone c of phant_id class c := @Pack T c T. + +Definition clone c of phant_id class c := @Pack T c. Definition pack b0 (m0 : real_axiom (num_for T b0)) := fun bT b & phant_id (NumDomain.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition numDomainType := @NumDomain.Pack cT xclass xT. + fun m & phant_id m0 m => Pack (@Class T b m). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition numDomainType := @NumDomain.Pack cT xclass. End ClassDef. @@ -590,30 +594,31 @@ Definition base2 R (c : class_of R) := RealDomain.Class (@mixin R c). Local Coercion base : class_of >-> NumField.class_of. Local Coercion base2 : class_of >-> RealDomain.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). + Definition pack := fun bT b & phant_id (NumField.class bT) (b : NumField.class_of T) => fun mT m & phant_id (RealDomain.class mT) (@RealDomain.Class T b m) => - Pack (@Class T b m) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition numDomainType := @NumDomain.Pack cT xclass xT. -Definition realDomainType := @RealDomain.Pack cT xclass xT. -Definition fieldType := @GRing.Field.Pack cT xclass xT. -Definition numFieldType := @NumField.Pack cT xclass xT. -Definition join_realDomainType := @RealDomain.Pack numFieldType xclass xT. + Pack (@Class T b m). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition numDomainType := @NumDomain.Pack cT xclass. +Definition realDomainType := @RealDomain.Pack cT xclass. +Definition fieldType := @GRing.Field.Pack cT xclass. +Definition numFieldType := @NumField.Pack cT xclass. +Definition join_realDomainType := @RealDomain.Pack numFieldType xclass. End ClassDef. @@ -663,30 +668,31 @@ Record class_of R := Class { base : RealField.class_of R; _ : archimedean_axiom (num_for R base) }. Local Coercion base : class_of >-> RealField.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition clone c of phant_id class c := @Pack T c T. + +Definition clone c of phant_id class c := @Pack T c. Definition pack b0 (m0 : archimedean_axiom (num_for T b0)) := fun bT b & phant_id (RealField.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition numDomainType := @NumDomain.Pack cT xclass xT. -Definition realDomainType := @RealDomain.Pack cT xclass xT. -Definition fieldType := @GRing.Field.Pack cT xclass xT. -Definition numFieldType := @NumField.Pack cT xclass xT. -Definition realFieldType := @RealField.Pack cT xclass xT. + fun m & phant_id m0 m => Pack (@Class T b m). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition numDomainType := @NumDomain.Pack cT xclass. +Definition realDomainType := @RealDomain.Pack cT xclass. +Definition fieldType := @GRing.Field.Pack cT xclass. +Definition numFieldType := @NumField.Pack cT xclass. +Definition realFieldType := @RealField.Pack cT xclass. End ClassDef. @@ -739,30 +745,31 @@ Record class_of R := Class { base : RealField.class_of R; _ : real_closed_axiom (num_for R base) }. Local Coercion base : class_of >-> RealField.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition clone c of phant_id class c := @Pack T c T. + +Definition clone c of phant_id class c := @Pack T c. Definition pack b0 (m0 : real_closed_axiom (num_for T b0)) := fun bT b & phant_id (RealField.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition comRingType := @GRing.ComRing.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. -Definition numDomainType := @NumDomain.Pack cT xclass xT. -Definition realDomainType := @RealDomain.Pack cT xclass xT. -Definition fieldType := @GRing.Field.Pack cT xclass xT. -Definition numFieldType := @NumField.Pack cT xclass xT. -Definition realFieldType := @RealField.Pack cT xclass xT. + fun m & phant_id m0 m => Pack (@Class T b m). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition comRingType := @GRing.ComRing.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. +Definition numDomainType := @NumDomain.Pack cT xclass. +Definition realDomainType := @RealDomain.Pack cT xclass. +Definition fieldType := @GRing.Field.Pack cT xclass. +Definition numFieldType := @NumField.Pack cT xclass. +Definition realFieldType := @RealField.Pack cT xclass. End ClassDef. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 542f8ad..75b2073 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -117,27 +117,27 @@ Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V). Structure class_of V := Class { base : GRing.Lmodule.class_of R V; - mixin : mixin_of (GRing.Lmodule.Pack _ base V) + mixin : mixin_of (GRing.Lmodule.Pack _ base) }. Local Coercion base : class_of >-> GRing.Lmodule.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (T : Type) (cT : type phR). -Definition class := let: Pack _ c _ := cT return class_of cT in c. -Definition clone c of phant_id class c := @Pack phR T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c := cT return class_of cT in c. +Definition clone c of phant_id class c := @Pack phR T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition dim := let: Mixin n _ := mixin class in n. -Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0 T)) := +Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0)) := fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b => - fun m & phant_id m0 m => Pack phR (@Class T b m) T. + fun m & phant_id m0 m => Pack phR (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. End ClassDef. Notation axiom n V := (axiom_def n (Phant V)). diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 7e86d3c..53a27f0 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -119,7 +119,7 @@ Definition BaseType T := fun c vAm & phant_id c (GRing.UnitRing.Class (BaseMixin vAm)) => fun (vT : vectType K) & phant vT & phant_id (Vector.mixin (Vector.class vT)) vAm => - @GRing.UnitRing.Pack T c T. + @GRing.UnitRing.Pack T c. End DefaultBase. @@ -129,41 +129,41 @@ Implicit Type phR : phant R. Record class_of A := Class { base1 : GRing.UnitAlgebra.class_of R A; - mixin : Vector.mixin_of (GRing.Lmodule.Pack _ base1 A) + mixin : Vector.mixin_of (GRing.Lmodule.Pack _ base1) }. Local Coercion base1 : class_of >-> GRing.UnitAlgebra.class_of. Definition base2 A c := @Vector.Class _ _ (@base1 A c) (mixin c). Local Coercion base2 : class_of >-> Vector.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (T : Type) (cT : type phR). -Definition class := let: Pack _ c _ := cT return class_of cT in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c := cT return class_of cT in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@GRing.UnitAlgebra.class R phR bT) (b : GRing.UnitAlgebra.class_of R T) => fun mT m & phant_id (@Vector.class R phR mT) (@Vector.Class R T b m) => - Pack (Phant R) (@Class T b m) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. -Definition ringType := @GRing.Ring.Pack cT xclass xT. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. -Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass xT. -Definition algType := @GRing.Algebra.Pack R phR cT xclass xT. -Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass xT. -Definition vectType := @Vector.Pack R phR cT xclass cT. -Definition vect_ringType := @GRing.Ring.Pack vectType xclass xT. -Definition vect_unitRingType := @GRing.UnitRing.Pack vectType xclass xT. -Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType xclass xT. -Definition vect_algType := @GRing.Algebra.Pack R phR vectType xclass xT. -Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType xclass xT. + Pack (Phant R) (@Class T b m). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. +Definition ringType := @GRing.Ring.Pack cT xclass. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass. +Definition lalgType := @GRing.Lalgebra.Pack R phR cT xclass. +Definition algType := @GRing.Algebra.Pack R phR cT xclass. +Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT xclass. +Definition vectType := @Vector.Pack R phR cT xclass. +Definition vect_ringType := @GRing.Ring.Pack vectType xclass. +Definition vect_unitRingType := @GRing.UnitRing.Pack vectType xclass. +Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType xclass. +Definition vect_algType := @GRing.Algebra.Pack R phR vectType xclass. +Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType xclass. End ClassDef. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 881b888..99db561 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -99,8 +99,8 @@ Variable R : ringType. Record class_of T := Class { base : Falgebra.class_of R T; comm_ext : commutative (Ring.mul base); - idomain_ext : IntegralDomain.axiom (Ring.Pack base T); - field_ext : Field.mixin_of (UnitRing.Pack base T) + idomain_ext : IntegralDomain.axiom (Ring.Pack base); + field_ext : Field.mixin_of (UnitRing.Pack base) }. Local Coercion base : class_of >-> Falgebra.class_of. @@ -117,12 +117,12 @@ Local Coercion base2 : class_of >-> ComUnitRing.class_of. Local Coercion base3 : class_of >-> IntegralDomain.class_of. Local Coercion base4 : class_of >-> Field.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (T : Type) (cT : type phR). -Definition class := let: Pack _ c _ := cT return class_of cT in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c := cT return class_of cT in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack := @@ -131,59 +131,59 @@ Definition pack := (b : Falgebra.class_of R T) => fun mT Cm IDm Fm & phant_id (Field.class mT) (@Field.Class T (@IntegralDomain.Class T (@ComUnitRing.Class T (@ComRing.Class T b - Cm) b) IDm) Fm) => Pack phR (@Class T b Cm IDm Fm) T. + Cm) b) IDm) Fm) => Pack phR (@Class T b Cm IDm Fm). Definition pack_eta K := let cK := Field.class K in let Cm := ComRing.mixin cK in let IDm := IntegralDomain.mixin cK in let Fm := Field.mixin cK in fun (bT : Falgebra.type phR) b & phant_id (Falgebra.class bT) b => - fun cT_ & phant_id (@Class T b) cT_ => @Pack phR T (cT_ Cm IDm Fm) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition unitRingType := @UnitRing.Pack cT xclass xT. -Definition comRingType := @ComRing.Pack cT xclass xT. -Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @IntegralDomain.Pack cT xclass xT. -Definition fieldType := @Field.Pack cT xclass xT. -Definition lmodType := @Lmodule.Pack R phR cT xclass xT. -Definition lalgType := @Lalgebra.Pack R phR cT xclass xT. -Definition algType := @Algebra.Pack R phR cT xclass xT. -Definition unitAlgType := @UnitAlgebra.Pack R phR cT xclass xT. -Definition vectType := @Vector.Pack R phR cT xclass xT. -Definition FalgType := @Falgebra.Pack R phR cT xclass xT. - -Definition Falg_comRingType := @ComRing.Pack FalgType xclass xT. -Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType xclass xT. -Definition Falg_idomainType := @IntegralDomain.Pack FalgType xclass xT. -Definition Falg_fieldType := @Field.Pack FalgType xclass xT. - -Definition vect_comRingType := @ComRing.Pack vectType xclass xT. -Definition vect_comUnitRingType := @ComUnitRing.Pack vectType xclass xT. -Definition vect_idomainType := @IntegralDomain.Pack vectType xclass xT. -Definition vect_fieldType := @Field.Pack vectType xclass xT. - -Definition unitAlg_comRingType := @ComRing.Pack unitAlgType xclass xT. -Definition unitAlg_comUnitRingType := @ComUnitRing.Pack unitAlgType xclass xT. -Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass xT. -Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass xT. - -Definition alg_comRingType := @ComRing.Pack algType xclass xT. -Definition alg_comUnitRingType := @ComUnitRing.Pack algType xclass xT. -Definition alg_idomainType := @IntegralDomain.Pack algType xclass xT. -Definition alg_fieldType := @Field.Pack algType xclass xT. - -Definition lalg_comRingType := @ComRing.Pack lalgType xclass xT. -Definition lalg_comUnitRingType := @ComUnitRing.Pack lalgType xclass xT. -Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass xT. -Definition lalg_fieldType := @Field.Pack lalgType xclass xT. - -Definition lmod_comRingType := @ComRing.Pack lmodType xclass xT. -Definition lmod_comUnitRingType := @ComUnitRing.Pack lmodType xclass xT. -Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass xT. -Definition lmod_fieldType := @Field.Pack lmodType xclass xT. + fun cT_ & phant_id (@Class T b) cT_ => @Pack phR T (cT_ Cm IDm Fm). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition unitRingType := @UnitRing.Pack cT xclass. +Definition comRingType := @ComRing.Pack cT xclass. +Definition comUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @IntegralDomain.Pack cT xclass. +Definition fieldType := @Field.Pack cT xclass. +Definition lmodType := @Lmodule.Pack R phR cT xclass. +Definition lalgType := @Lalgebra.Pack R phR cT xclass. +Definition algType := @Algebra.Pack R phR cT xclass. +Definition unitAlgType := @UnitAlgebra.Pack R phR cT xclass. +Definition vectType := @Vector.Pack R phR cT xclass. +Definition FalgType := @Falgebra.Pack R phR cT xclass. + +Definition Falg_comRingType := @ComRing.Pack FalgType xclass. +Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType xclass. +Definition Falg_idomainType := @IntegralDomain.Pack FalgType xclass. +Definition Falg_fieldType := @Field.Pack FalgType xclass. + +Definition vect_comRingType := @ComRing.Pack vectType xclass. +Definition vect_comUnitRingType := @ComUnitRing.Pack vectType xclass. +Definition vect_idomainType := @IntegralDomain.Pack vectType xclass. +Definition vect_fieldType := @Field.Pack vectType xclass. + +Definition unitAlg_comRingType := @ComRing.Pack unitAlgType xclass. +Definition unitAlg_comUnitRingType := @ComUnitRing.Pack unitAlgType xclass. +Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass. +Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass. + +Definition alg_comRingType := @ComRing.Pack algType xclass. +Definition alg_comUnitRingType := @ComUnitRing.Pack algType xclass. +Definition alg_idomainType := @IntegralDomain.Pack algType xclass. +Definition alg_fieldType := @Field.Pack algType xclass. + +Definition lalg_comRingType := @ComRing.Pack lalgType xclass. +Definition lalg_comUnitRingType := @ComUnitRing.Pack lalgType xclass. +Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass. +Definition lalg_fieldType := @Field.Pack lalgType xclass. + +Definition lmod_comRingType := @ComRing.Pack lmodType xclass. +Definition lmod_comUnitRingType := @ComUnitRing.Pack lmodType xclass. +Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass. +Definition lmod_fieldType := @Field.Pack lmodType xclass. End FieldExt. diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index 2421b16..4197a2e 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -138,7 +138,7 @@ Variables (F : finFieldType) (T : finType). Section Vector. Variable cvT : Vector.class_of F T. -Let vT := Vector.Pack (Phant F) cvT T. +Let vT := Vector.Pack (Phant F) cvT. Lemma card_vspace (V : {vspace vT}) : #|V| = (#|F| ^ \dim V)%N. Proof. @@ -159,7 +159,7 @@ Proof. by apply: eq_card => v; rewrite (@memvf _ vT). Qed. End Vector. Variable caT : Falgebra.class_of F T. -Let aT := Falgebra.Pack (Phant F) caT T. +Let aT := Falgebra.Pack (Phant F) caT. Lemma card_vspace1 : #|(1%VS : {vspace aT})| = #|F|. Proof. by rewrite card_vspace (dimv1 aT). Qed. @@ -691,7 +691,7 @@ Definition FinDomainFieldType : finFieldType := let dom_class := @GRing.IntegralDomain.Class R com_unit_class domR in let field_class := @GRing.Field.Class R dom_class finDomain_field in let finfield_class := @FinRing.Field.Class R field_class fin_unit_class in - FinRing.Field.Pack finfield_class R. + FinRing.Field.Pack finfield_class. Definition FinDomainSplittingFieldType p (charRp : p \in [char R]) := let RoverFp := @primeChar_splittingFieldType p FinDomainFieldType charRp in diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 2ed40e1..252868d 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -345,38 +345,38 @@ Definition axiom (L : fieldExtType F) := exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}. Record class_of (L : Type) : Type := - Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base L)}. + Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base)}. Local Coercion base : class_of >-> FieldExt.class_of. -Structure type (phF : phant F) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phF : phant F) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variable (phF : phant F) (T : Type) (cT : type phF). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). -Definition clone c of phant_id class c := @Pack phF T c T. +Definition clone c of phant_id class c := @Pack phF T c. -Definition pack b0 (ax0 : axiom (@FieldExt.Pack F (Phant F) T b0 T)) := +Definition pack b0 (ax0 : axiom (@FieldExt.Pack F (Phant F) T b0)) := fun bT b & phant_id (@FieldExt.class F phF bT) b => - fun ax & phant_id ax0 ax => Pack (Phant F) (@Class T b ax) T. - -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @Zmodule.Pack cT xclass xT. -Definition ringType := @Ring.Pack cT xclass xT. -Definition unitRingType := @UnitRing.Pack cT xclass xT. -Definition comRingType := @ComRing.Pack cT xclass xT. -Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT. -Definition idomainType := @IntegralDomain.Pack cT xclass xT. -Definition fieldType := @Field.Pack cT xclass xT. -Definition lmodType := @Lmodule.Pack F phF cT xclass xT. -Definition lalgType := @Lalgebra.Pack F phF cT xclass xT. -Definition algType := @Algebra.Pack F phF cT xclass xT. -Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass xT. -Definition vectType := @Vector.Pack F phF cT xclass xT. -Definition FalgType := @Falgebra.Pack F phF cT xclass xT. -Definition fieldExtType := @FieldExt.Pack F phF cT xclass xT. + fun ax & phant_id ax0 ax => Pack (Phant F) (@Class T b ax). + +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @Zmodule.Pack cT xclass. +Definition ringType := @Ring.Pack cT xclass. +Definition unitRingType := @UnitRing.Pack cT xclass. +Definition comRingType := @ComRing.Pack cT xclass. +Definition comUnitRingType := @ComUnitRing.Pack cT xclass. +Definition idomainType := @IntegralDomain.Pack cT xclass. +Definition fieldType := @Field.Pack cT xclass. +Definition lmodType := @Lmodule.Pack F phF cT xclass. +Definition lalgType := @Lalgebra.Pack F phF cT xclass. +Definition algType := @Algebra.Pack F phF cT xclass. +Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass. +Definition vectType := @Vector.Pack F phF cT xclass. +Definition FalgType := @Falgebra.Pack F phF cT xclass. +Definition fieldExtType := @FieldExt.Pack F phF cT xclass. End ClassDef. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index a68bc9f..19cefcd 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -302,10 +302,10 @@ Local Notation T := (arg_sort bT). Local Notation rT := (sort bT). Local Notation class := (finClass bT). -Canonical eqType := Equality.Pack class rT. -Canonical choiceType := Choice.Pack class rT. -Canonical countType := Countable.Pack class rT. -Canonical finType := Finite.Pack class rT. +Canonical eqType := Equality.Pack class. +Canonical choiceType := Choice.Pack class. +Canonical countType := Countable.Pack class. +Canonical finType := Finite.Pack class. Definition arg_eqType := Eval hnf in [eqType of T]. Definition arg_choiceType := Eval hnf in [choiceType of T]. Definition arg_countType := Eval hnf in [countType of T]. diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index baa7231..6f46832 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -255,19 +255,19 @@ Record mixin_of T := Mixin { Record class_of T := Class {base : Equality.class_of T; mixin : mixin_of T}. Local Coercion base : class_of >-> Equality.class_of. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack m := - fun b bT & phant_id (Equality.class bT) b => Pack (@Class T b m) T. + fun b bT & phant_id (Equality.class bT) b => Pack (@Class T b m). (* Inheritance *) -Definition eqType := @Equality.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. End ClassDef. @@ -408,7 +408,7 @@ Variables (P : pred T) (sT : subType P). Definition sub_choiceMixin := PcanChoiceMixin (@valK T P sT). Definition sub_choiceClass := @Choice.Class sT (sub_eqMixin sT) sub_choiceMixin. -Canonical sub_choiceType := Choice.Pack sub_choiceClass sT. +Canonical sub_choiceType := Choice.Pack sub_choiceClass. End SubChoice. @@ -522,19 +522,19 @@ Section ClassDef. Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }. Local Coercion base : class_of >-> Choice.class_of. -Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}. +Structure type : Type := Pack {sort : Type; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack m := - fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T. + fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. End ClassDef. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 7473ed7..a5e8784 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -126,13 +126,13 @@ Notation class_of := mixin_of (only parsing). Section ClassDef. -Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ := cT return class_of cT in c. +Definition class := let: Pack _ c := cT return class_of cT in c. -Definition pack c := @Pack T c T. +Definition pack c := @Pack T c. Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c. End ClassDef. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index d4f564f..8be2eb0 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -172,7 +172,7 @@ Section Mixins. Variable T : countType. Definition EnumMixin := - let: Countable.Pack _ (Countable.Class _ m) _ as cT := T + let: Countable.Pack _ (Countable.Class _ m) as cT := T return forall e : seq cT, axiom e -> mixin_of cT in @Mixin (EqType _ _) m. @@ -198,26 +198,26 @@ Section ClassDef. Record class_of T := Class { base : Choice.class_of T; - mixin : mixin_of (Equality.Pack base T) + mixin : mixin_of (Equality.Pack base) }. Definition base2 T c := Countable.Class (@base T c) (mixin_base (mixin c)). Local Coercion base : class_of >-> Choice.class_of. -Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}. +Structure type : Type := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. +Definition clone c of phant_id class c := @Pack T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition pack b0 (m0 : mixin_of (EqType T b0)) := fun bT b & phant_id (Choice.class bT) b => - fun m & phant_id m0 m => Pack (@Class T b m) T. + fun m & phant_id m0 m => Pack (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition countType := @Countable.Pack cT (base2 xclass) xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition countType := @Countable.Pack cT (base2 xclass). End ClassDef. @@ -1379,7 +1379,7 @@ Coercion subFinType_subCountType sT := @SubCountType _ _ sT (subFin_mixin sT). Canonical subFinType_subCountType. Coercion subFinType_finType sT := - Pack (@Class sT (sub_choiceClass sT) (subFin_mixin sT)) sT. + Pack (@Class sT (sub_choiceClass sT) (subFin_mixin sT)). Canonical subFinType_finType. Lemma codom_val sT x : (x \in codom (val : sT -> T)) = P x. diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index 1475d55..ea929d7 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -128,11 +128,10 @@ Notation quot_class_of := quot_mixin_of. Record quotType := QuotTypePack { quot_sort :> Type; - quot_class : quot_class_of quot_sort; - _ : Type + quot_class : quot_class_of quot_sort }. -Definition QuotType_pack qT m := @QuotTypePack qT m qT. +Definition QuotType_pack qT m := @QuotTypePack qT m. Variable qT : quotType. Definition pi_phant of phant qT := quot_pi (quot_class qT). @@ -143,7 +142,7 @@ Lemma repr_ofK : cancel repr_of \pi. Proof. by rewrite /pi_phant /repr_of /=; case: qT=> [? []]. Qed. Definition QuotType_clone (Q : Type) qT cT - of phant_id (quot_class qT) cT := @QuotTypePack Q cT Q. + of phant_id (quot_class qT) cT := @QuotTypePack Q cT. End QuotientDef. @@ -329,8 +328,8 @@ Variable eq_quot_op : rel T. Definition eq_quot_mixin_of (Q : Type) (qc : quot_class_of T Q) (ec : Equality.class_of Q) := - {mono \pi_(QuotTypePack qc Q) : x y / - eq_quot_op x y >-> @eq_op (Equality.Pack ec Q) x y}. + {mono \pi_(QuotTypePack qc) : x y / + eq_quot_op x y >-> @eq_op (Equality.Pack ec) x y}. Record eq_quot_class_of (Q : Type) : Type := EqQuotClass { eq_quot_quot_class :> quot_class_of T Q; @@ -341,13 +340,13 @@ Record eq_quot_class_of (Q : Type) : Type := EqQuotClass { Record eqQuotType : Type := EqQuotTypePack { eq_quot_sort :> Type; _ : eq_quot_class_of eq_quot_sort; - _ : Type + }. Implicit Type eqT : eqQuotType. Definition eq_quot_class eqT : eq_quot_class_of eqT := - let: EqQuotTypePack _ cT _ as qT' := eqT return eq_quot_class_of qT' in cT. + let: EqQuotTypePack _ cT as qT' := eqT return eq_quot_class_of qT' in cT. Canonical eqQuotType_eqType eqT := EqType eqT (eq_quot_class eqT). Canonical eqQuotType_quotType eqT := QuotType eqT (eq_quot_class eqT). @@ -358,10 +357,10 @@ Coercion eqQuotType_quotType : eqQuotType >-> quotType. Definition EqQuotType_pack Q := fun (qT : quotType T) (eT : eqType) qc ec of phant_id (quot_class qT) qc & phant_id (Equality.class eT) ec => - fun m => EqQuotTypePack (@EqQuotClass Q qc ec m) Q. + fun m => EqQuotTypePack (@EqQuotClass Q qc ec m). Definition EqQuotType_clone (Q : Type) eqT cT - of phant_id (eq_quot_class eqT) cT := @EqQuotTypePack Q cT Q. + of phant_id (eq_quot_class eqT) cT := @EqQuotTypePack Q cT. Lemma pi_eq_quot eqT : {mono \pi_eqT : x y / eq_quot_op x y >-> x == y}. Proof. by case: eqT => [] ? []. Qed. |