diff options
| -rw-r--r-- | .github/workflows/nix.yml | 2 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 72 | ||||
| -rw-r--r-- | mathcomp/Make | 1 | ||||
| -rw-r--r-- | mathcomp/Make.test-suite | 1 | ||||
| -rw-r--r-- | mathcomp/_CoqProject | 1 | ||||
| -rw-r--r-- | mathcomp/algebra/countalg.v | 375 | ||||
| -rw-r--r-- | mathcomp/algebra/finalg.v | 617 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 284 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 373 | ||||
| -rw-r--r-- | mathcomp/algebra/vector.v | 14 | ||||
| -rw-r--r-- | mathcomp/field/falgebra.v | 34 | ||||
| -rw-r--r-- | mathcomp/field/fieldext.v | 102 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 42 | ||||
| -rw-r--r-- | mathcomp/ssreflect/choice.v | 14 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 10 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 378 | ||||
| -rw-r--r-- | mathcomp/test_suite/test_regular_conv.v | 34 |
17 files changed, 1157 insertions, 1197 deletions
diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index 8446b1c..0ea5aee 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -8,7 +8,7 @@ jobs: strategy: fail-fast: false matrix: - coq: [ "8.11", "8.10", "8.9", "8.8", "8.7" ] + coq: [ "8.11", "8.10", "8.9" ] steps: - name: Get branch shortname run: echo "##[set-output name=name;]$(echo ${GITHUB_REF#refs/heads/})" diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 4eaf1ee..99fe690 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -82,12 +82,6 @@ make-coq-latest: - merge_requests - schedules -coq-8.7: - extends: .opam-build-once - -coq-8.8: - extends: .opam-build-once - coq-8.9: extends: .opam-build-once @@ -173,16 +167,6 @@ test-coq-8.9: variables: COQ_VERSION: "8.9" -test-coq-8.8: - extends: .test-once - variables: - COQ_VERSION: "8.8" - -test-coq-8.7: - extends: .test-once - variables: - COQ_VERSION: "8.7" - # set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using .ci: stage: test @@ -228,16 +212,6 @@ test-coq-8.7: - merge_requests - schedules -ci-fourcolor-8.7: - extends: .ci-fourcolor - variables: - COQ_VERSION: "8.7" - -ci-fourcolor-8.8: - extends: .ci-fourcolor - variables: - COQ_VERSION: "8.8" - ci-fourcolor-8.9: extends: .ci-fourcolor variables: @@ -277,16 +251,6 @@ ci-fourcolor-dev: - merge_requests - schedules -ci-odd-order-8.7: - extends: .ci-odd-order - variables: - COQ_VERSION: "8.7" - -ci-odd-order-8.8: - extends: .ci-odd-order - variables: - COQ_VERSION: "8.8" - ci-odd-order-8.9: extends: .ci-odd-order variables: @@ -352,16 +316,6 @@ ci-lemma-overloading-dev: - opam pin add -n -k path coq-mathcomp-bigenough . - opam install -y -v -j "${NJOBS}" coq-mathcomp-bigenough -ci-bigenough-8.7: - extends: .ci-bigenough - variables: - COQ_VERSION: "8.7" - -ci-bigenough-8.8: - extends: .ci-bigenough - variables: - COQ_VERSION: "8.8" - ci-bigenough-8.9: extends: .ci-bigenough variables: @@ -398,16 +352,6 @@ ci-bigenough-dev: # - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-real-closed # - opam install -y -v -j "${NJOBS}" coq-mathcomp-real-closed # -# ci-real-closed-8.7: -# extends: .ci-real-closed -# variables: -# COQ_VERSION: "8.7" -# -# ci-real-closed-8.8: -# extends: .ci-real-closed -# variables: -# COQ_VERSION: "8.8" -# # ci-real-closed-8.9: # extends: .ci-real-closed # variables: @@ -455,16 +399,6 @@ ci-bigenough-dev: - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-finmap - opam install -y -v -j "${NJOBS}" coq-mathcomp-finmap -ci-finmap-8.7: - extends: .ci-finmap - variables: - COQ_VERSION: "8.7" - -ci-finmap-8.8: - extends: .ci-finmap - variables: - COQ_VERSION: "8.8" - ci-finmap-8.9: extends: .ci-finmap variables: @@ -557,12 +491,6 @@ ci-fcsl-pcm-dev: except: - schedules -mathcomp-dev:coq-8.7: - extends: .docker-deploy-once - -mathcomp-dev:coq-8.8: - extends: .docker-deploy-once - mathcomp-dev:coq-8.9: extends: .docker-deploy-once diff --git a/mathcomp/Make b/mathcomp/Make index 1d837c1..828a9e8 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -98,3 +98,4 @@ ssreflect/tuple.v -arg -w -arg -notation-overridden -arg -w -arg -duplicate-clear -arg -w -arg -ambiguous-paths +-arg -w -arg +non-primitive-record diff --git a/mathcomp/Make.test-suite b/mathcomp/Make.test-suite index f34958d..acfbf89 100644 --- a/mathcomp/Make.test-suite +++ b/mathcomp/Make.test-suite @@ -1,6 +1,7 @@ test_suite/test_hierarchy_all.v test_suite/test_ssrAC.v test_suite/test_guard.v +test_suite/test_regular_conv.v -I . diff --git a/mathcomp/_CoqProject b/mathcomp/_CoqProject index 912cc1a..3b204ba 100644 --- a/mathcomp/_CoqProject +++ b/mathcomp/_CoqProject @@ -5,3 +5,4 @@ -arg -w -arg -redundant-canonical-projection -arg -w -arg -notation-overridden -arg -w -arg -duplicate-clear +-arg -w -arg +non-primitive-record diff --git a/mathcomp/algebra/countalg.v b/mathcomp/algebra/countalg.v index 3aaa02d..0fa953b 100644 --- a/mathcomp/algebra/countalg.v +++ b/mathcomp/algebra/countalg.v @@ -62,8 +62,10 @@ Module Zmodule. Section ClassDef. +Set Primitive Projections. Record class_of M := Class { base : GRing.Zmodule.class_of M; mixin : mixin_of M }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.Zmodule.class_of. Local Coercion mixin : class_of >-> mixin_of. @@ -72,15 +74,13 @@ 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. -Notation xclass := (class : class_of 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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (cnt_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. -Definition join_countType := @Countable.Pack zmodType (cnt_ xclass). +Definition join_countType := @Countable.Pack zmodType (cnt_ class). End ClassDef. @@ -110,7 +110,9 @@ Module Ring. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.Ring.class_of R; mixin : mixin_of R }. +Unset Primitive Projections. 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. @@ -120,17 +122,15 @@ 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. -Notation xclass := (class : class_of 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. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (cnt_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition join_countType := @Countable.Pack ringType (cnt_ class). +Definition join_countZmodType := @Zmodule.Pack ringType class. End ClassDef. @@ -165,8 +165,10 @@ Module ComRing. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.ComRing.class_of R; mixin : mixin_of R }. +Unset Primitive Projections. 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. @@ -176,20 +178,18 @@ 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. -Notation xclass := (class : class_of 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. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (cnt_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition join_countType := @Countable.Pack comRingType (cnt_ class). +Definition join_countZmodType := @Zmodule.Pack comRingType class. +Definition join_countRingType := @Ring.Pack comRingType class. End ClassDef. @@ -229,8 +229,10 @@ Module UnitRing. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.UnitRing.class_of R; mixin : mixin_of R }. +Unset Primitive Projections. 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. @@ -240,21 +242,19 @@ 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. -Notation xclass := (class : class_of 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). -Definition join_countZmodType := @Zmodule.Pack unitRingType xclass. -Definition join_countRingType := @Ring.Pack unitRingType xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (cnt_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @Ring.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. + +Definition join_countType := @Countable.Pack unitRingType (cnt_ class). +Definition join_countZmodType := @Zmodule.Pack unitRingType class. +Definition join_countRingType := @Ring.Pack unitRingType class. End ClassDef. @@ -294,8 +294,10 @@ Module ComUnitRing. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.ComUnitRing.class_of R; mixin : mixin_of R }. +Unset Primitive Projections. Definition base2 R (c : class_of R) := ComRing.Class (base c) (mixin c). Definition base3 R (c : class_of R) := @UnitRing.Class R (base c) (mixin c). Local Coercion base : class_of >-> GRing.ComUnitRing.class_of. @@ -307,31 +309,28 @@ 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. -Notation xclass := (class : class_of 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. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (cnt_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition countComRingType := @ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. + +Definition join_countType := @Countable.Pack comUnitRingType (cnt_ class). +Definition join_countZmodType := @Zmodule.Pack comUnitRingType class. +Definition join_countRingType := @Ring.Pack comUnitRingType class. +Definition join_countComRingType := @ComRing.Pack comUnitRingType class. +Definition join_countUnitRingType := @UnitRing.Pack comUnitRingType class. +Definition ujoin_countComRingType := @ComRing.Pack unitRingType class. +Definition cjoin_countUnitRingType := @UnitRing.Pack comRingType class. +Definition ccjoin_countUnitRingType := @UnitRing.Pack countComRingType class. End ClassDef. @@ -385,8 +384,10 @@ Module IntegralDomain. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.IntegralDomain.class_of R; mixin : mixin_of R }. +Unset Primitive Projections. 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. @@ -396,30 +397,28 @@ 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. -Notation xclass := (class : class_of 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. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (cnt_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition countComRingType := @ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition countComUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. + +Definition join_countType := @Countable.Pack idomainType (cnt_ class). +Definition join_countZmodType := @Zmodule.Pack idomainType class. +Definition join_countRingType := @Ring.Pack idomainType class. +Definition join_countUnitRingType := @UnitRing.Pack idomainType class. +Definition join_countComRingType := @ComRing.Pack idomainType class. +Definition join_countComUnitRingType := @ComUnitRing.Pack idomainType class. End ClassDef. @@ -474,8 +473,10 @@ Module Field. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.Field.class_of R; mixin : mixin_of R }. +Unset Primitive Projections. 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. @@ -485,33 +486,31 @@ 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. -Notation xclass := (class : class_of 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. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (cnt_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition countComRingType := @ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition countComUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition countIdomainType := @IntegralDomain.Pack cT class. +Definition fieldType := @GRing.Field.Pack cT class. + +Definition join_countType := @Countable.Pack fieldType (cnt_ class). +Definition join_countZmodType := @Zmodule.Pack fieldType class. +Definition join_countRingType := @Ring.Pack fieldType class. +Definition join_countUnitRingType := @UnitRing.Pack fieldType class. +Definition join_countComRingType := @ComRing.Pack fieldType class. +Definition join_countComUnitRingType := @ComUnitRing.Pack fieldType class. +Definition join_countIdomainType := @IntegralDomain.Pack fieldType class. End ClassDef. @@ -571,8 +570,10 @@ Module DecidableField. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.DecidableField.class_of R; mixin : mixin_of R }. +Unset Primitive Projections. 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. @@ -582,37 +583,34 @@ 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. -Notation xclass := (class : class_of 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. -Definition join_countIdomainType := @IntegralDomain.Pack decFieldType xclass. -Definition join_countFieldType := @Field.Pack decFieldType xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (cnt_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition countComRingType := @ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition countComUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition countIdomainType := @IntegralDomain.Pack cT class. +Definition fieldType := @GRing.Field.Pack cT class. +Definition countFieldType := @Field.Pack cT class. +Definition decFieldType := @GRing.DecidableField.Pack cT class. + +Definition join_countType := @Countable.Pack decFieldType (cnt_ class). +Definition join_countZmodType := @Zmodule.Pack decFieldType class. +Definition join_countRingType := @Ring.Pack decFieldType class. +Definition join_countUnitRingType := @UnitRing.Pack decFieldType class. +Definition join_countComRingType := @ComRing.Pack decFieldType class. +Definition join_countComUnitRingType := @ComUnitRing.Pack decFieldType class. +Definition join_countIdomainType := @IntegralDomain.Pack decFieldType class. +Definition join_countFieldType := @Field.Pack decFieldType class. End ClassDef. @@ -677,8 +675,10 @@ Module ClosedField. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.ClosedField.class_of R; mixin : mixin_of R }. +Unset Primitive Projections. 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. @@ -688,42 +688,37 @@ 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. -Notation xclass := (class : class_of 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. -Definition join_countIdomainType := - @IntegralDomain.Pack closedFieldType xclass. -Definition join_countFieldType := @Field.Pack closedFieldType xclass. -Definition join_countDecFieldType := - @DecidableField.Pack closedFieldType xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (cnt_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition countComRingType := @ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition countComUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition countIdomainType := @IntegralDomain.Pack cT class. +Definition fieldType := @GRing.Field.Pack cT class. +Definition countFieldType := @Field.Pack cT class. +Definition decFieldType := @GRing.DecidableField.Pack cT class. +Definition countDecFieldType := @DecidableField.Pack cT class. +Definition closedFieldType := @GRing.ClosedField.Pack cT class. + +Definition join_countType := @Countable.Pack closedFieldType (cnt_ class). +Definition join_countZmodType := @Zmodule.Pack closedFieldType class. +Definition join_countRingType := @Ring.Pack closedFieldType class. +Definition join_countUnitRingType := @UnitRing.Pack closedFieldType class. +Definition join_countComRingType := @ComRing.Pack closedFieldType class. +Definition join_countComUnitRingType := @ComUnitRing.Pack closedFieldType class. +Definition join_countIdomainType := @IntegralDomain.Pack closedFieldType class. +Definition join_countFieldType := @Field.Pack closedFieldType class. +Definition join_countDecFieldType := @DecidableField.Pack closedFieldType class. End ClassDef. diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index 607e023..04ac263 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -74,8 +74,10 @@ Module Zmodule. Section ClassDef. +Set Primitive Projections. Record class_of M := Class { base : GRing.Zmodule.class_of M; mixin : mixin_of M base }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.Zmodule.class_of. Local Coercion base2 R (c : class_of R) : CountRing.Zmodule.class_of R := CountRing.Zmodule.Class c (mixin c). @@ -86,22 +88,20 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition zmod_finType := @Finite.Pack zmodType (fin_ xclass). +Definition zmod_finType := @Finite.Pack zmodType (fin_ class). Definition zmod_baseFinGroupType := base_group zmodType zmodType finType. Definition zmod_finGroupType := fin_group zmod_baseFinGroupType zmodType. -Definition countZmod_finType := @Finite.Pack countZmodType (fin_ xclass). +Definition countZmod_finType := @Finite.Pack countZmodType (fin_ class). Definition countZmod_baseFinGroupType := base_group countZmodType zmodType finType. Definition countZmod_finGroupType := @@ -171,8 +171,10 @@ Module Ring. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.Ring.class_of R; mixin : mixin_of R base }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.Ring.class_of. Local Coercion base2 R (c : class_of R) : CountRing.Ring.class_of R := CountRing.Ring.Class c (mixin c). @@ -184,31 +186,29 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition ringType := @GRing.Ring.Pack cT xclass. -Definition countRingType := @CountRing.Ring.Pack cT xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @CountRing.Ring.Pack cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition ring_finType := @Finite.Pack ringType (fin_ xclass). +Definition ring_finType := @Finite.Pack ringType (fin_ class). Definition ring_baseFinGroupType := base_group ringType zmodType finType. Definition ring_finGroupType := fin_group ring_baseFinGroupType zmodType. -Definition ring_finZmodType := @Zmodule.Pack ringType xclass. -Definition countRing_finType := @Finite.Pack countRingType (fin_ xclass). +Definition ring_finZmodType := @Zmodule.Pack ringType class. +Definition countRing_finType := @Finite.Pack countRingType (fin_ class). Definition countRing_baseFinGroupType := base_group countRingType zmodType finType. Definition countRing_finGroupType := fin_group countRing_baseFinGroupType zmodType. -Definition countRing_finZmodType := @Zmodule.Pack countRingType xclass. +Definition countRing_finZmodType := @Zmodule.Pack countRingType class. End ClassDef. @@ -295,8 +295,10 @@ Module ComRing. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.ComRing.class_of R; mixin : mixin_of R base }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.ComRing.class_of. Local Coercion base2 R (c : class_of R) : CountRing.ComRing.class_of R := CountRing.ComRing.Class c (mixin c). @@ -308,36 +310,34 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition ringType := @GRing.Ring.Pack cT xclass. -Definition countRingType := @CountRing.Ring.Pack cT xclass. -Definition finRingType := @Ring.Pack cT xclass. -Definition comRingType := @GRing.ComRing.Pack cT xclass. -Definition countComRingType := @CountRing.ComRing.Pack cT xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @CountRing.Ring.Pack cT class. +Definition finRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition countComRingType := @CountRing.ComRing.Pack cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition comRing_finType := @Finite.Pack comRingType (fin_ xclass). +Definition comRing_finType := @Finite.Pack comRingType (fin_ class). Definition comRing_baseFinGroupType := base_group comRingType zmodType finType. Definition comRing_finGroupType := fin_group comRing_baseFinGroupType zmodType. -Definition comRing_finZmodType := @Zmodule.Pack comRingType xclass. -Definition comRing_finRingType := @Ring.Pack comRingType xclass. -Definition countComRing_finType := @Finite.Pack countComRingType (fin_ xclass). +Definition comRing_finZmodType := @Zmodule.Pack comRingType class. +Definition comRing_finRingType := @Ring.Pack comRingType class. +Definition countComRing_finType := @Finite.Pack countComRingType (fin_ class). Definition countComRing_baseFinGroupType := base_group countComRingType zmodType finType. Definition countComRing_finGroupType := fin_group countComRing_baseFinGroupType zmodType. -Definition countComRing_finZmodType := @Zmodule.Pack countComRingType xclass. -Definition countComRing_finRingType := @Ring.Pack countComRingType xclass. +Definition countComRing_finZmodType := @Zmodule.Pack countComRingType class. +Definition countComRing_finRingType := @Ring.Pack countComRingType class. End ClassDef. @@ -397,8 +397,10 @@ Module UnitRing. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.UnitRing.class_of R; mixin : mixin_of R base }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.UnitRing.class_of. Local Coercion base2 R (c : class_of R) : CountRing.UnitRing.class_of R := CountRing.UnitRing.Class c (mixin c). @@ -410,39 +412,37 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition ringType := @GRing.Ring.Pack cT xclass. -Definition countRingType := @CountRing.Ring.Pack cT xclass. -Definition finRingType := @Ring.Pack cT xclass. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass. -Definition countUnitRingType := @CountRing.UnitRing.Pack cT xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @CountRing.Ring.Pack cT class. +Definition finRingType := @Ring.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @CountRing.UnitRing.Pack cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition unitRing_finType := @Finite.Pack unitRingType (fin_ xclass). +Definition unitRing_finType := @Finite.Pack unitRingType (fin_ class). Definition unitRing_baseFinGroupType := base_group unitRingType zmodType finType. Definition unitRing_finGroupType := fin_group unitRing_baseFinGroupType zmodType. -Definition unitRing_finZmodType := @Zmodule.Pack unitRingType xclass. -Definition unitRing_finRingType := @Ring.Pack unitRingType xclass. +Definition unitRing_finZmodType := @Zmodule.Pack unitRingType class. +Definition unitRing_finRingType := @Ring.Pack unitRingType class. Definition countUnitRing_finType := - @Finite.Pack countUnitRingType (fin_ xclass). + @Finite.Pack countUnitRingType (fin_ class). Definition countUnitRing_baseFinGroupType := base_group countUnitRingType zmodType finType. Definition countUnitRing_finGroupType := fin_group countUnitRing_baseFinGroupType zmodType. -Definition countUnitRing_finZmodType := @Zmodule.Pack countUnitRingType xclass. -Definition countUnitRing_finRingType := @Ring.Pack countUnitRingType xclass. +Definition countUnitRing_finZmodType := @Zmodule.Pack countUnitRingType class. +Definition countUnitRing_finRingType := @Ring.Pack countUnitRingType class. End ClassDef. @@ -583,8 +583,10 @@ Module ComUnitRing. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.ComUnitRing.class_of R; mixin : mixin_of R base }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.ComUnitRing.class_of. Local Coercion base2 R (c : class_of R) : CountRing.ComUnitRing.class_of R := CountRing.ComUnitRing.Class c (mixin c). @@ -598,60 +600,58 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition ringType := @GRing.Ring.Pack cT xclass. -Definition countRingType := @CountRing.Ring.Pack cT xclass. -Definition finRingType := @Ring.Pack cT xclass. -Definition comRingType := @GRing.ComRing.Pack cT xclass. -Definition countComRingType := @CountRing.ComRing.Pack cT xclass. -Definition finComRingType := @ComRing.Pack cT xclass. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass. -Definition countUnitRingType := @CountRing.UnitRing.Pack cT xclass. -Definition finUnitRingType := @UnitRing.Pack cT xclass. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. -Definition countComUnitRingType := @CountRing.ComUnitRing.Pack cT xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @CountRing.Ring.Pack cT class. +Definition finRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition countComRingType := @CountRing.ComRing.Pack cT class. +Definition finComRingType := @ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @CountRing.UnitRing.Pack cT class. +Definition finUnitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition countComUnitRingType := @CountRing.ComUnitRing.Pack cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition comUnitRing_finType := @Finite.Pack comUnitRingType (fin_ xclass). +Definition comUnitRing_finType := @Finite.Pack comUnitRingType (fin_ class). Definition comUnitRing_baseFinGroupType := base_group comUnitRingType zmodType finType. Definition comUnitRing_finGroupType := fin_group comUnitRing_baseFinGroupType zmodType. -Definition comUnitRing_finZmodType := @Zmodule.Pack comUnitRingType xclass. -Definition comUnitRing_finRingType := @Ring.Pack comUnitRingType xclass. -Definition comUnitRing_finComRingType := @ComRing.Pack comUnitRingType xclass. -Definition comUnitRing_finUnitRingType := @UnitRing.Pack comUnitRingType xclass. +Definition comUnitRing_finZmodType := @Zmodule.Pack comUnitRingType class. +Definition comUnitRing_finRingType := @Ring.Pack comUnitRingType class. +Definition comUnitRing_finComRingType := @ComRing.Pack comUnitRingType class. +Definition comUnitRing_finUnitRingType := @UnitRing.Pack comUnitRingType class. Definition countComUnitRing_finType := - @Finite.Pack countComUnitRingType (fin_ xclass). + @Finite.Pack countComUnitRingType (fin_ class). Definition countComUnitRing_baseFinGroupType := base_group countComUnitRingType zmodType finType. Definition countComUnitRing_finGroupType := fin_group countComUnitRing_baseFinGroupType zmodType. Definition countComUnitRing_finZmodType := - @Zmodule.Pack countComUnitRingType xclass. + @Zmodule.Pack countComUnitRingType class. Definition countComUnitRing_finRingType := - @Ring.Pack countComUnitRingType xclass. + @Ring.Pack countComUnitRingType class. Definition countComUnitRing_finComRingType := - @ComRing.Pack countComUnitRingType xclass. + @ComRing.Pack countComUnitRingType class. Definition countComUnitRing_finUnitRingType := - @UnitRing.Pack countComUnitRingType xclass. -Definition unitRing_finComRingType := @ComRing.Pack unitRingType xclass. + @UnitRing.Pack countComUnitRingType class. +Definition unitRing_finComRingType := @ComRing.Pack unitRingType class. Definition countUnitRing_finComRingType := - @ComRing.Pack countUnitRingType xclass. -Definition comRing_finUnitRingType := @UnitRing.Pack comRingType xclass. + @ComRing.Pack countUnitRingType class. +Definition comRing_finUnitRingType := @UnitRing.Pack comRingType class. Definition countComRing_finUnitRingType := - @UnitRing.Pack countComRingType xclass. -Definition finComRing_finUnitRingType := @UnitRing.Pack finComRingType xclass. + @UnitRing.Pack countComRingType class. +Definition finComRing_finUnitRingType := @UnitRing.Pack finComRingType class. End ClassDef. @@ -733,8 +733,10 @@ Module IntegralDomain. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.IntegralDomain.class_of R; mixin : mixin_of R base }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.IntegralDomain.class_of. Local Coercion base2 R (c : class_of R) : CountRing.IntegralDomain.class_of R := CountRing.IntegralDomain.Class c (mixin c). @@ -746,53 +748,51 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition ringType := @GRing.Ring.Pack cT xclass. -Definition countRingType := @CountRing.Ring.Pack cT xclass. -Definition finRingType := @Ring.Pack cT xclass. -Definition comRingType := @GRing.ComRing.Pack cT xclass. -Definition countComRingType := @CountRing.ComRing.Pack cT xclass. -Definition finComRingType := @ComRing.Pack cT xclass. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass. -Definition countUnitRingType := @CountRing.UnitRing.Pack cT xclass. -Definition finUnitRingType := @UnitRing.Pack cT xclass. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. -Definition countComUnitRingType := @CountRing.ComUnitRing.Pack cT xclass. -Definition finComUnitRingType := @ComUnitRing.Pack cT xclass. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. -Definition countIdomainType := @CountRing.IntegralDomain.Pack cT xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @CountRing.Ring.Pack cT class. +Definition finRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition countComRingType := @CountRing.ComRing.Pack cT class. +Definition finComRingType := @ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @CountRing.UnitRing.Pack cT class. +Definition finUnitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition countComUnitRingType := @CountRing.ComUnitRing.Pack cT class. +Definition finComUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition countIdomainType := @CountRing.IntegralDomain.Pack cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition idomain_finType := @Finite.Pack idomainType (fin_ xclass). +Definition idomain_finType := @Finite.Pack idomainType (fin_ class). Definition idomain_baseFinGroupType := base_group idomainType zmodType finType. Definition idomain_finGroupType := fin_group idomain_baseFinGroupType zmodType. -Definition idomain_finZmodType := @Zmodule.Pack idomainType xclass. -Definition idomain_finRingType := @Ring.Pack idomainType xclass. -Definition idomain_finUnitRingType := @UnitRing.Pack idomainType xclass. -Definition idomain_finComRingType := @ComRing.Pack idomainType xclass. -Definition idomain_finComUnitRingType := @ComUnitRing.Pack idomainType xclass. -Definition countIdomain_finType := @Finite.Pack countIdomainType (fin_ xclass). +Definition idomain_finZmodType := @Zmodule.Pack idomainType class. +Definition idomain_finRingType := @Ring.Pack idomainType class. +Definition idomain_finUnitRingType := @UnitRing.Pack idomainType class. +Definition idomain_finComRingType := @ComRing.Pack idomainType class. +Definition idomain_finComUnitRingType := @ComUnitRing.Pack idomainType class. +Definition countIdomain_finType := @Finite.Pack countIdomainType (fin_ class). Definition countIdomain_baseFinGroupType := base_group countIdomainType zmodType finType. Definition countIdomain_finGroupType := fin_group countIdomain_baseFinGroupType zmodType. -Definition countIdomain_finZmodType := @Zmodule.Pack countIdomainType xclass. -Definition countIdomain_finRingType := @Ring.Pack countIdomainType xclass. +Definition countIdomain_finZmodType := @Zmodule.Pack countIdomainType class. +Definition countIdomain_finRingType := @Ring.Pack countIdomainType class. Definition countIdomain_finUnitRingType := - @UnitRing.Pack countIdomainType xclass. -Definition countIdomain_finComRingType := @ComRing.Pack countIdomainType xclass. + @UnitRing.Pack countIdomainType class. +Definition countIdomain_finComRingType := @ComRing.Pack countIdomainType class. Definition countIdomain_finComUnitRingType := - @ComUnitRing.Pack countIdomainType xclass. + @ComUnitRing.Pack countIdomainType class. End ClassDef. @@ -876,8 +876,10 @@ Module Field. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : GRing.Field.class_of R; mixin : mixin_of R base }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.Field.class_of. Local Coercion base2 R (c : class_of R) : CountRing.Field.class_of R := CountRing.Field.Class c (mixin c). @@ -889,58 +891,56 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition ringType := @GRing.Ring.Pack cT xclass. -Definition countRingType := @CountRing.Ring.Pack cT xclass. -Definition finRingType := @Ring.Pack cT xclass. -Definition comRingType := @GRing.ComRing.Pack cT xclass. -Definition countComRingType := @CountRing.ComRing.Pack cT xclass. -Definition finComRingType := @ComRing.Pack cT xclass. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass. -Definition countUnitRingType := @CountRing.UnitRing.Pack cT xclass. -Definition finUnitRingType := @UnitRing.Pack cT xclass. -Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass. -Definition countComUnitRingType := @CountRing.ComUnitRing.Pack cT xclass. -Definition finComUnitRingType := @ComUnitRing.Pack cT xclass. -Definition idomainType := @GRing.IntegralDomain.Pack cT xclass. -Definition countIdomainType := @CountRing.IntegralDomain.Pack cT xclass. -Definition finIdomainType := @IntegralDomain.Pack cT xclass. -Definition fieldType := @GRing.Field.Pack cT xclass. -Definition countFieldType := @CountRing.Field.Pack cT xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @CountRing.Ring.Pack cT class. +Definition finRingType := @Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition countComRingType := @CountRing.ComRing.Pack cT class. +Definition finComRingType := @ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @CountRing.UnitRing.Pack cT class. +Definition finUnitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition countComUnitRingType := @CountRing.ComUnitRing.Pack cT class. +Definition finComUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition countIdomainType := @CountRing.IntegralDomain.Pack cT class. +Definition finIdomainType := @IntegralDomain.Pack cT class. +Definition fieldType := @GRing.Field.Pack cT class. +Definition countFieldType := @CountRing.Field.Pack cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition field_finType := @Finite.Pack fieldType (fin_ xclass). +Definition field_finType := @Finite.Pack fieldType (fin_ class). Definition field_baseFinGroupType := base_group fieldType zmodType finType. Definition field_finGroupType := fin_group field_baseFinGroupType zmodType. -Definition field_finZmodType := @Zmodule.Pack fieldType xclass. -Definition field_finRingType := @Ring.Pack fieldType xclass. -Definition field_finUnitRingType := @UnitRing.Pack fieldType xclass. -Definition field_finComRingType := @ComRing.Pack fieldType xclass. -Definition field_finComUnitRingType := @ComUnitRing.Pack fieldType xclass. -Definition field_finIdomainType := @IntegralDomain.Pack fieldType xclass. -Definition countField_finType := @Finite.Pack countFieldType (fin_ xclass). +Definition field_finZmodType := @Zmodule.Pack fieldType class. +Definition field_finRingType := @Ring.Pack fieldType class. +Definition field_finUnitRingType := @UnitRing.Pack fieldType class. +Definition field_finComRingType := @ComRing.Pack fieldType class. +Definition field_finComUnitRingType := @ComUnitRing.Pack fieldType class. +Definition field_finIdomainType := @IntegralDomain.Pack fieldType class. +Definition countField_finType := @Finite.Pack countFieldType (fin_ class). Definition countField_baseFinGroupType := base_group countFieldType zmodType finType. Definition countField_finGroupType := fin_group countField_baseFinGroupType zmodType. -Definition countField_finZmodType := @Zmodule.Pack countFieldType xclass. -Definition countField_finRingType := @Ring.Pack countFieldType xclass. -Definition countField_finUnitRingType := @UnitRing.Pack countFieldType xclass. -Definition countField_finComRingType := @ComRing.Pack countFieldType xclass. +Definition countField_finZmodType := @Zmodule.Pack countFieldType class. +Definition countField_finRingType := @Ring.Pack countFieldType class. +Definition countField_finUnitRingType := @UnitRing.Pack countFieldType class. +Definition countField_finComRingType := @ComRing.Pack countFieldType class. Definition countField_finComUnitRingType := - @ComUnitRing.Pack countFieldType xclass. + @ComUnitRing.Pack countFieldType class. Definition countField_finIdomainType := - @IntegralDomain.Pack countFieldType xclass. + @IntegralDomain.Pack countFieldType class. End ClassDef. @@ -1066,17 +1066,16 @@ Module DecField. Section Joins. Variable cT : Field.type. -Let xT := let: Field.Pack T _ := cT in T. -Let xclass : Field.class_of xT := Field.class cT. +Let class : Field.class_of cT := Field.class cT. Definition type := Eval hnf in DecFieldType cT (DecidableFieldMixin cT). -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 finType := @Finite.Pack type (fin_ class). +Definition finZmodType := @Zmodule.Pack type class. +Definition finRingType := @Ring.Pack type class. +Definition finUnitRingType := @UnitRing.Pack type class. +Definition finComRingType := @ComRing.Pack type class. +Definition finComUnitRingType := @ComUnitRing.Pack type class. +Definition finIdomainType := @IntegralDomain.Pack type class. Definition baseFinGroupType := base_group type finZmodType finZmodType. Definition finGroupType := fin_group baseFinGroupType cT. @@ -1105,8 +1104,10 @@ Section ClassDef. Variable R : ringType. +Set Primitive Projections. Record class_of M := Class { base : GRing.Lmodule.class_of R M; mixin : mixin_of M base }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.Lmodule.class_of. Local Coercion base2 R (c : class_of R) : Zmodule.class_of R := Zmodule.Class (mixin c). @@ -1116,26 +1117,24 @@ 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 pack := gen_pack (Pack phR) Class (@GRing.Lmodule.class R phR). -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. + +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition lmodType := @GRing.Lmodule.Pack R phR cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition lmod_countType := @Countable.Pack lmodType (fin_ xclass). -Definition lmod_finType := @Finite.Pack lmodType (fin_ xclass). +Definition lmod_countType := @Countable.Pack lmodType (fin_ class). +Definition lmod_finType := @Finite.Pack lmodType (fin_ class). Definition lmod_baseFinGroupType := base_group lmodType zmodType finType. Definition lmod_finGroupType := fin_group lmod_baseFinGroupType zmodType. -Definition lmod_countZmodType := @CountRing.Zmodule.Pack lmodType xclass. -Definition lmod_finZmodType := @Zmodule.Pack lmodType xclass. +Definition lmod_countZmodType := @CountRing.Zmodule.Pack lmodType class. +Definition lmod_finZmodType := @Zmodule.Pack lmodType class. End ClassDef. @@ -1184,8 +1183,10 @@ Section ClassDef. Variable R : ringType. +Set Primitive Projections. Record class_of M := Class { base : GRing.Lalgebra.class_of R M; mixin : mixin_of M base }. +Unset Primitive Projections. Definition base2 M (c : class_of M) := Ring.Class (mixin c). Definition base3 M (c : class_of M) := @Lmodule.Class _ _ (base c) (mixin c). Local Coercion base : class_of >-> GRing.Lalgebra.class_of. @@ -1197,39 +1198,37 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition ringType := @GRing.Ring.Pack cT xclass. -Definition countRingType := @CountRing.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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @CountRing.Ring.Pack cT class. +Definition finRingType := @Ring.Pack cT class. +Definition lmodType := @GRing.Lmodule.Pack R phR cT class. +Definition finLmodType := @Lmodule.Pack R phR cT class. +Definition lalgType := @GRing.Lalgebra.Pack R phR cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition lalg_countType := @Countable.Pack lalgType (fin_ xclass). -Definition lalg_finType := @Finite.Pack lalgType (fin_ xclass). +Definition lalg_countType := @Countable.Pack lalgType (fin_ class). +Definition lalg_finType := @Finite.Pack lalgType (fin_ class). Definition lalg_baseFinGroupType := base_group lalgType zmodType finType. Definition lalg_finGroupType := fin_group lalg_baseFinGroupType zmodType. -Definition lalg_countZmodType := @CountRing.Zmodule.Pack lalgType xclass. -Definition lalg_finZmodType := @Zmodule.Pack lalgType xclass. -Definition lalg_finLmodType := @Lmodule.Pack R phR lalgType xclass. -Definition lalg_countRingType := @CountRing.Ring.Pack lalgType xclass. -Definition lalg_finRingType := @Ring.Pack lalgType xclass. -Definition lmod_countRingType := @CountRing.Ring.Pack lmodType xclass. -Definition lmod_finRingType := @Ring.Pack lmodType xclass. -Definition finLmod_ringType := @GRing.Ring.Pack finLmodType xclass. -Definition finLmod_countRingType := @CountRing.Ring.Pack finLmodType xclass. -Definition finLmod_finRingType := @Ring.Pack finLmodType xclass. +Definition lalg_countZmodType := @CountRing.Zmodule.Pack lalgType class. +Definition lalg_finZmodType := @Zmodule.Pack lalgType class. +Definition lalg_finLmodType := @Lmodule.Pack R phR lalgType class. +Definition lalg_countRingType := @CountRing.Ring.Pack lalgType class. +Definition lalg_finRingType := @Ring.Pack lalgType class. +Definition lmod_countRingType := @CountRing.Ring.Pack lmodType class. +Definition lmod_finRingType := @Ring.Pack lmodType class. +Definition finLmod_ringType := @GRing.Ring.Pack finLmodType class. +Definition finLmod_countRingType := @CountRing.Ring.Pack finLmodType class. +Definition finLmod_finRingType := @Ring.Pack finLmodType class. End ClassDef. @@ -1297,8 +1296,10 @@ Section ClassDef. Variable R : ringType. +Set Primitive Projections. Record class_of M := Class { base : GRing.Algebra.class_of R M; mixin : mixin_of M base }. +Unset Primitive Projections. 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. @@ -1308,37 +1309,35 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition ringType := @GRing.Ring.Pack cT xclass. -Definition countRingType := @CountRing.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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @CountRing.Ring.Pack cT class. +Definition finRingType := @Ring.Pack cT class. +Definition lmodType := @GRing.Lmodule.Pack R phR cT class. +Definition finLmodType := @Lmodule.Pack R phR cT class. +Definition lalgType := @GRing.Lalgebra.Pack R phR cT class. +Definition finLalgType := @Lalgebra.Pack R phR cT class. +Definition algType := @GRing.Algebra.Pack R phR cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition alg_countType := @Countable.Pack algType (fin_ xclass). -Definition alg_finType := @Finite.Pack algType (fin_ xclass). +Definition alg_countType := @Countable.Pack algType (fin_ class). +Definition alg_finType := @Finite.Pack algType (fin_ class). Definition alg_baseFinGroupType := base_group algType zmodType finType. Definition alg_finGroupType := fin_group alg_baseFinGroupType zmodType. -Definition alg_countZmodType := @CountRing.Zmodule.Pack algType xclass. -Definition alg_finZmodType := @Zmodule.Pack algType xclass. -Definition alg_countRingType := @CountRing.Ring.Pack algType xclass. -Definition alg_finRingType := @Ring.Pack algType xclass. -Definition alg_finLmodType := @Lmodule.Pack R phR algType xclass. -Definition alg_finLalgType := @Lalgebra.Pack R phR algType xclass. +Definition alg_countZmodType := @CountRing.Zmodule.Pack algType class. +Definition alg_finZmodType := @Zmodule.Pack algType class. +Definition alg_countRingType := @CountRing.Ring.Pack algType class. +Definition alg_finRingType := @Ring.Pack algType class. +Definition alg_finLmodType := @Lmodule.Pack R phR algType class. +Definition alg_finLalgType := @Lalgebra.Pack R phR algType class. End ClassDef. @@ -1405,8 +1404,10 @@ Section ClassDef. Variable R : unitRingType. +Set Primitive Projections. Record class_of M := Class { base : GRing.UnitAlgebra.class_of R M; mixin : mixin_of M base }. +Unset Primitive Projections. Definition base2 M (c : class_of M) := Algebra.Class (mixin c). Definition base3 M (c : class_of M) := @UnitRing.Class _ (base c) (mixin c). @@ -1419,73 +1420,71 @@ 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. -Notation xclass := (class : class_of 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 countZmodType := @CountRing.Zmodule.Pack cT xclass. -Definition finZmodType := @Zmodule.Pack cT xclass. -Definition ringType := @GRing.Ring.Pack cT xclass. -Definition countRingType := @CountRing.Ring.Pack cT xclass. -Definition finRingType := @Ring.Pack cT xclass. -Definition unitRingType := @GRing.UnitRing.Pack cT xclass. -Definition countUnitRingType := @CountRing.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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (fin_ class). +Definition finType := @Finite.Pack cT (fin_ class). +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition countZmodType := @CountRing.Zmodule.Pack cT class. +Definition finZmodType := @Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition countRingType := @CountRing.Ring.Pack cT class. +Definition finRingType := @Ring.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition countUnitRingType := @CountRing.UnitRing.Pack cT class. +Definition finUnitRingType := @UnitRing.Pack cT class. +Definition lmodType := @GRing.Lmodule.Pack R phR cT class. +Definition finLmodType := @Lmodule.Pack R phR cT class. +Definition lalgType := @GRing.Lalgebra.Pack R phR cT class. +Definition finLalgType := @Lalgebra.Pack R phR cT class. +Definition algType := @GRing.Algebra.Pack R phR cT class. +Definition finAlgType := @Algebra.Pack R phR cT class. +Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT class. Definition baseFinGroupType := base_group cT zmodType finType. Definition finGroupType := fin_group baseFinGroupType zmodType. -Definition unitAlg_countType := @Countable.Pack unitAlgType (fin_ xclass). -Definition unitAlg_finType := @Finite.Pack unitAlgType (fin_ xclass). +Definition unitAlg_countType := @Countable.Pack unitAlgType (fin_ class). +Definition unitAlg_finType := @Finite.Pack unitAlgType (fin_ class). Definition unitAlg_baseFinGroupType := base_group unitAlgType zmodType finType. Definition unitAlg_finGroupType := fin_group unitAlg_baseFinGroupType zmodType. -Definition unitAlg_countZmodType := @CountRing.Zmodule.Pack unitAlgType xclass. -Definition unitAlg_finZmodType := @Zmodule.Pack unitAlgType xclass. -Definition unitAlg_countRingType := @CountRing.Ring.Pack unitAlgType xclass. -Definition unitAlg_finRingType := @Ring.Pack unitAlgType xclass. +Definition unitAlg_countZmodType := @CountRing.Zmodule.Pack unitAlgType class. +Definition unitAlg_finZmodType := @Zmodule.Pack unitAlgType class. +Definition unitAlg_countRingType := @CountRing.Ring.Pack unitAlgType class. +Definition unitAlg_finRingType := @Ring.Pack unitAlgType class. Definition unitAlg_countUnitRingType := - @CountRing.UnitRing.Pack unitAlgType xclass. -Definition unitAlg_finUnitRingType := @UnitRing.Pack unitAlgType xclass. -Definition unitAlg_finLmodType := @Lmodule.Pack R phR unitAlgType xclass. -Definition unitAlg_finLalgType := @Lalgebra.Pack R phR unitAlgType xclass. -Definition unitAlg_finAlgType := @Algebra.Pack R phR unitAlgType xclass. -Definition unitRing_finLmodType := @Lmodule.Pack R phR unitRingType xclass. -Definition unitRing_finLalgType := @Lalgebra.Pack R phR unitRingType xclass. -Definition unitRing_finAlgType := @Algebra.Pack R phR unitRingType xclass. + @CountRing.UnitRing.Pack unitAlgType class. +Definition unitAlg_finUnitRingType := @UnitRing.Pack unitAlgType class. +Definition unitAlg_finLmodType := @Lmodule.Pack R phR unitAlgType class. +Definition unitAlg_finLalgType := @Lalgebra.Pack R phR unitAlgType class. +Definition unitAlg_finAlgType := @Algebra.Pack R phR unitAlgType class. +Definition unitRing_finLmodType := @Lmodule.Pack R phR unitRingType class. +Definition unitRing_finLalgType := @Lalgebra.Pack R phR unitRingType class. +Definition unitRing_finAlgType := @Algebra.Pack R phR unitRingType class. Definition countUnitRing_lmodType := - @GRing.Lmodule.Pack R phR countUnitRingType xclass. + @GRing.Lmodule.Pack R phR countUnitRingType class. Definition countUnitRing_finLmodType := - @Lmodule.Pack R phR countUnitRingType xclass. + @Lmodule.Pack R phR countUnitRingType class. Definition countUnitRing_lalgType := - @GRing.Lalgebra.Pack R phR countUnitRingType xclass. + @GRing.Lalgebra.Pack R phR countUnitRingType class. Definition countUnitRing_finLalgType := - @Lalgebra.Pack R phR countUnitRingType xclass. + @Lalgebra.Pack R phR countUnitRingType class. Definition countUnitRing_algType := - @GRing.Algebra.Pack R phR countUnitRingType xclass. + @GRing.Algebra.Pack R phR countUnitRingType class. Definition countUnitRing_finAlgType := - @Algebra.Pack R phR countUnitRingType xclass. + @Algebra.Pack R phR countUnitRingType class. Definition finUnitRing_lmodType := - @GRing.Lmodule.Pack R phR finUnitRingType xclass. + @GRing.Lmodule.Pack R phR finUnitRingType class. Definition finUnitRing_finLmodType := - @Lmodule.Pack R phR finUnitRingType xclass. + @Lmodule.Pack R phR finUnitRingType class. Definition finUnitRing_lalgType := - @GRing.Lalgebra.Pack R phR finUnitRingType xclass. + @GRing.Lalgebra.Pack R phR finUnitRingType class. Definition finUnitRing_finLalgType := - @Lalgebra.Pack R phR finUnitRingType xclass. + @Lalgebra.Pack R phR finUnitRingType class. Definition finUnitRing_algType := - @GRing.Algebra.Pack R phR finUnitRingType xclass. + @GRing.Algebra.Pack R phR finUnitRingType class. Definition finUnitRing_finAlgType := - @Algebra.Pack R phR finUnitRingType xclass. + @Algebra.Pack R phR finUnitRingType class. End ClassDef. diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 6128fa0..97766c1 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -635,7 +635,9 @@ Record mixin_of (V : Type) : Type := Mixin { Section ClassDef. +Set Primitive Projections. Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }. +Unset Primitive Projections. Local Coercion base : class_of >-> Choice.class_of. Structure type := Pack {sort; _ : class_of sort}. @@ -643,14 +645,12 @@ 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. -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). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. End ClassDef. @@ -916,10 +916,12 @@ Definition EtaMixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 := Section ClassDef. +Set Primitive Projections. Record class_of (R : Type) : Type := Class { base : Zmodule.class_of R; mixin : mixin_of (Zmodule.Pack base) }. +Unset Primitive Projections. Local Coercion base : class_of >-> Zmodule.class_of. Structure type := Pack {sort; _ : class_of sort}. @@ -927,16 +929,14 @@ 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. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). 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). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition zmodType := @Zmodule.Pack cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. End ClassDef. @@ -1533,10 +1533,12 @@ Section ClassDef. Variable R : ringType. -Structure class_of V := Class { +Set Primitive Projections. +Record class_of V := Class { base : Zmodule.class_of V; mixin : mixin_of R (Zmodule.Pack base) }. +Unset Primitive Projections. Local Coercion base : class_of >-> Zmodule.class_of. Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. @@ -1544,16 +1546,14 @@ 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. -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)) := fun bT b & phant_id (Zmodule.class bT) b => fun m & phant_id m0 m => Pack phR (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition zmodType := @Zmodule.Pack cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. End ClassDef. @@ -1688,11 +1688,13 @@ Section ClassDef. Variable R : ringType. +Set Primitive Projections. Record class_of (T : Type) : Type := Class { base : Ring.class_of T; mixin : Lmodule.mixin_of R (Zmodule.Pack base); ext : @axiom R (Lmodule.Pack _ (Lmodule.Class mixin)) (Ring.mul base) }. +Unset Primitive Projections. 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. @@ -1702,8 +1704,6 @@ 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. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0) mul0) := fun bT b & phant_id (Ring.class bT) (b : Ring.class_of T) => @@ -1711,12 +1711,12 @@ Definition pack b0 mul0 (axT : @axiom R (@Lmodule.Pack R _ T b0) mul0) := fun ax & phant_id axT ax => Pack (Phant R) (@Class T b m 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 lmodType := @Lmodule.Pack R phR cT xclass. -Definition lmod_ringType := @Lmodule.Pack R phR ringType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition lmodType := @Lmodule.Pack R phR cT class. +Definition lmod_ringType := @Lmodule.Pack R phR ringType class. End ClassDef. @@ -2501,8 +2501,10 @@ Definition RingMixin R one mul mulA mulC mul1x mul_addl := Section ClassDef. +Set Primitive Projections. Record class_of R := Class {base : Ring.class_of R; mixin : commutative (Ring.mul base)}. +Unset Primitive Projections. Local Coercion base : class_of >-> Ring.class_of. Structure type := Pack {sort; _ : class_of sort}. @@ -2510,17 +2512,15 @@ 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. -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). -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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. End ClassDef. @@ -2661,10 +2661,12 @@ Section ClassDef. Variable R : ringType. +Set Primitive Projections. Record class_of (T : Type) : Type := Class { base : Lalgebra.class_of R T; mixin : axiom (Lalgebra.Pack _ base) }. +Unset Primitive Projections. Local Coercion base : class_of >-> Lalgebra.class_of. Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. @@ -2672,19 +2674,17 @@ 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. -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). -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. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition lmodType := @Lmodule.Pack R phR cT class. +Definition lalgType := @Lalgebra.Pack R phR cT class. End ClassDef. @@ -2723,10 +2723,12 @@ Section ClassDef. Variable R : ringType. +Set Primitive Projections. Record class_of (T : Type) : Type := Class { base : Algebra.class_of R T; mixin : commutative (Ring.mul base) }. +Unset Primitive Projections. Definition base2 R m := ComRing.Class (@mixin R m). Local Coercion base : class_of >-> Algebra.class_of. Local Coercion base2 : class_of >-> ComRing.class_of. @@ -2735,25 +2737,23 @@ 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. -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 (ComRing.mixin (ComRing.class mT)) m => 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 comRingType := @ComRing.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_comRingType := @Lmodule.Pack R phR comRingType xclass. -Definition lalg_comRingType := @Lalgebra.Pack R phR comRingType xclass. -Definition alg_comRingType := @Algebra.Pack R phR comRingType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition comRingType := @ComRing.Pack cT class. +Definition lmodType := @Lmodule.Pack R phR cT class. +Definition lalgType := @Lalgebra.Pack R phR cT class. +Definition algType := @Algebra.Pack R phR cT class. +Definition lmod_comRingType := @Lmodule.Pack R phR comRingType class. +Definition lalg_comRingType := @Lalgebra.Pack R phR comRingType class. +Definition alg_comRingType := @Algebra.Pack R phR comRingType class. End ClassDef. @@ -2858,10 +2858,12 @@ Definition EtaMixin R unit inv mulVr mulrV unitP inv_out := Section ClassDef. +Set Primitive Projections. Record class_of (R : Type) : Type := Class { base : Ring.class_of R; mixin : mixin_of (Ring.Pack base) }. +Unset Primitive Projections. Local Coercion base : class_of >-> Ring.class_of. Structure type := Pack {sort; _ : class_of sort}. @@ -2869,17 +2871,15 @@ 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. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). 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). -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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. End ClassDef. @@ -3186,10 +3186,12 @@ End Mixin. Section ClassDef. +Set Primitive Projections. Record class_of (R : Type) : Type := Class { base : ComRing.class_of R; mixin : UnitRing.mixin_of (Ring.Pack base) }. +Unset Primitive Projections. 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. @@ -3198,21 +3200,19 @@ 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. -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). -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. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition comRingType := @ComRing.Pack cT class. +Definition unitRingType := @UnitRing.Pack cT class. +Definition com_unitRingType := @UnitRing.Pack comRingType class. End ClassDef. @@ -3250,10 +3250,12 @@ Section ClassDef. Variable R : ringType. +Set Primitive Projections. Record class_of (T : Type) : Type := Class { base : Algebra.class_of R T; mixin : GRing.UnitRing.mixin_of (Ring.Pack base) }. +Unset Primitive Projections. 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. @@ -3262,25 +3264,23 @@ 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. -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). -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. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition unitRingType := @UnitRing.Pack cT class. +Definition lmodType := @Lmodule.Pack R phR cT class. +Definition lalgType := @Lalgebra.Pack R phR cT class. +Definition algType := @Algebra.Pack R phR cT class. +Definition lmod_unitRingType := @Lmodule.Pack R phR unitRingType class. +Definition lalg_unitRingType := @Lalgebra.Pack R phR unitRingType class. +Definition alg_unitRingType := @Algebra.Pack R phR unitRingType class. End ClassDef. @@ -3322,10 +3322,12 @@ Section ClassDef. Variable R : ringType. +Set Primitive Projections. Record class_of (T : Type) : Type := Class { base : ComAlgebra.class_of R T; mixin : GRing.UnitRing.mixin_of (ComRing.Pack base) }. +Unset Primitive Projections. Definition base2 R m := UnitAlgebra.Class (@mixin R m). Definition base3 R m := ComUnitRing.Class (@mixin R m). Local Coercion base : class_of >-> ComAlgebra.class_of. @@ -3336,36 +3338,34 @@ 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. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@ComAlgebra.class R phR bT) (b : ComAlgebra.class_of R T) => fun mT m & phant_id (UnitRing.mixin (UnitRing.class mT)) m => 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 comRingType := @ComRing.Pack cT xclass. -Definition comUnitRingType := @ComUnitRing.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 comAlgType := @ComAlgebra.Pack R phR cT xclass. -Definition unitAlgType := @UnitAlgebra.Pack R phR cT xclass. -Definition comalg_unitRingType := @ComAlgebra.Pack R phR unitRingType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition unitRingType := @UnitRing.Pack cT class. +Definition comRingType := @ComRing.Pack cT class. +Definition comUnitRingType := @ComUnitRing.Pack cT class. +Definition lmodType := @Lmodule.Pack R phR cT class. +Definition lalgType := @Lalgebra.Pack R phR cT class. +Definition algType := @Algebra.Pack R phR cT class. +Definition comAlgType := @ComAlgebra.Pack R phR cT class. +Definition unitAlgType := @UnitAlgebra.Pack R phR cT class. +Definition comalg_unitRingType := @ComAlgebra.Pack R phR unitRingType class. Definition comalg_comUnitRingType := - @ComAlgebra.Pack R phR comUnitRingType xclass. -Definition comalg_unitAlgType := @ComAlgebra.Pack R phR unitAlgType xclass. -Definition unitalg_comRingType := @UnitAlgebra.Pack R phR comRingType xclass. + @ComAlgebra.Pack R phR comUnitRingType class. +Definition comalg_unitAlgType := @ComAlgebra.Pack R phR unitAlgType class. +Definition unitalg_comRingType := @UnitAlgebra.Pack R phR comRingType class. Definition unitalg_comUnitRingType := - @UnitAlgebra.Pack R phR comUnitRingType xclass. -Definition lmod_comUnitRingType := @Lmodule.Pack R phR comUnitRingType xclass. -Definition lalg_comUnitRingType := @Lalgebra.Pack R phR comUnitRingType xclass. -Definition alg_comUnitRingType := @Algebra.Pack R phR comUnitRingType xclass. + @UnitAlgebra.Pack R phR comUnitRingType class. +Definition lmod_comUnitRingType := @Lmodule.Pack R phR comUnitRingType class. +Definition lalg_comUnitRingType := @Lalgebra.Pack R phR comUnitRingType class. +Definition alg_comUnitRingType := @Algebra.Pack R phR comUnitRingType class. End ClassDef. @@ -4563,8 +4563,10 @@ Definition axiom (R : ringType) := Section ClassDef. +Set Primitive Projections. Record class_of (R : Type) : Type := Class {base : ComUnitRing.class_of R; mixin : axiom (Ring.Pack base)}. +Unset Primitive Projections. Local Coercion base : class_of >-> ComUnitRing.class_of. Structure type := Pack {sort; _ : class_of sort}. @@ -4572,20 +4574,18 @@ 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. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). 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). -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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition comRingType := @ComRing.Pack cT class. +Definition unitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @ComUnitRing.Pack cT class. End ClassDef. @@ -4778,10 +4778,12 @@ End Mixins. Section ClassDef. +Set Primitive Projections. Record class_of (F : Type) : Type := Class { base : IntegralDomain.class_of F; mixin : mixin_of (UnitRing.Pack base) }. +Unset Primitive Projections. Local Coercion base : class_of >-> IntegralDomain.class_of. Structure type := Pack {sort; _ : class_of sort}. @@ -4789,21 +4791,19 @@ 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. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). 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). -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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition comRingType := @ComRing.Pack cT class. +Definition unitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @IntegralDomain.Pack cT class. End ClassDef. @@ -5033,8 +5033,10 @@ Record mixin_of (R : unitRingType) : Type := Section ClassDef. +Set Primitive Projections. Record class_of (F : Type) : Type := Class {base : Field.class_of F; mixin : mixin_of (UnitRing.Pack base)}. +Unset Primitive Projections. Local Coercion base : class_of >-> Field.class_of. Structure type := Pack {sort; _ : class_of sort}. @@ -5042,22 +5044,20 @@ 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. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). 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). -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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition comRingType := @ComRing.Pack cT class. +Definition unitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @IntegralDomain.Pack cT class. +Definition fieldType := @Field.Pack cT class. End ClassDef. @@ -5275,8 +5275,10 @@ Definition axiom (R : ringType) := Section ClassDef. +Set Primitive Projections. Record class_of (F : Type) : Type := - Class {base : DecidableField.class_of F; _ : axiom (Ring.Pack base)}. + Class {base : DecidableField.class_of F; mixin : axiom (Ring.Pack base)}. +Unset Primitive Projections. Local Coercion base : class_of >-> DecidableField.class_of. Structure type := Pack {sort; _ : class_of sort}. @@ -5284,8 +5286,6 @@ 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. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) := fun bT b & phant_id (DecidableField.class bT) b => @@ -5294,15 +5294,15 @@ Definition pack b0 (m0 : axiom (@Ring.Pack T b0)) := (* There should eventually be a constructor from polynomial resolution *) (* that builds the DecidableField mixin using QE. *) -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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition comRingType := @ComRing.Pack cT class. +Definition unitRingType := @UnitRing.Pack cT class. +Definition comUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @IntegralDomain.Pack cT class. +Definition fieldType := @Field.Pack cT class. Definition decFieldType := @DecidableField.Pack cT class. End ClassDef. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 2ebbdcc..2eefe8e 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -169,12 +169,14 @@ Local Notation ring_for T b := (@GRing.Ring.Pack T b). Module NumDomain. Section ClassDef. +Set Primitive Projections. Record class_of T := Class { base : GRing.IntegralDomain.class_of T; order_mixin : Order.POrder.mixin_of (Equality.class (ring_for T base)); normed_mixin : normed_mixin_of (ring_for T base) order_mixin; mixin : mixin_of normed_mixin; }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.IntegralDomain.class_of. Local Coercion order_base T (class_of_T : class_of T) := @@ -184,8 +186,6 @@ 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. -Notation xclass := (class : class_of xT). Definition clone c of phant_id class c := @Pack T c. Definition pack (b0 : GRing.IntegralDomain.class_of _) om0 (nm0 : @normed_mixin_of (ring_for T b0) (ring_for T b0) om0) @@ -197,21 +197,21 @@ Definition pack (b0 : GRing.IntegralDomain.class_of _) om0 fun m & phant_id m0 m => @Pack T (@Class T b om nm 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 porderType := @Order.POrder.Pack ring_display cT xclass. -Definition porder_zmodType := @GRing.Zmodule.Pack porderType xclass. -Definition porder_ringType := @GRing.Ring.Pack porderType xclass. -Definition porder_comRingType := @GRing.ComRing.Pack porderType xclass. -Definition porder_unitRingType := @GRing.UnitRing.Pack porderType xclass. -Definition porder_comUnitRingType := @GRing.ComUnitRing.Pack porderType xclass. -Definition porder_idomainType := @GRing.IntegralDomain.Pack porderType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition porderType := @Order.POrder.Pack ring_display cT class. +Definition porder_zmodType := @GRing.Zmodule.Pack porderType class. +Definition porder_ringType := @GRing.Ring.Pack porderType class. +Definition porder_comRingType := @GRing.ComRing.Pack porderType class. +Definition porder_unitRingType := @GRing.UnitRing.Pack porderType class. +Definition porder_comUnitRingType := @GRing.ComUnitRing.Pack porderType class. +Definition porder_idomainType := @GRing.IntegralDomain.Pack porderType class. End ClassDef. @@ -264,10 +264,12 @@ Section ClassDef. Variable R : numDomainType. +Set Primitive Projections. Record class_of (T : Type) := Class { base : GRing.Zmodule.class_of T; mixin : @normed_mixin_of R (@GRing.Zmodule.Pack T base) (NumDomain.class R); }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.Zmodule.class_of. Local Coercion mixin : class_of >-> normed_mixin_of. @@ -280,15 +282,13 @@ 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. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack b0 (m0 : @normed_mixin_of R (@GRing.Zmodule.Pack T b0) (NumDomain.class R)) := Pack phR (@Class T b0 m0). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. End ClassDef. @@ -330,26 +330,24 @@ Section NumDomain_joins. Variables (T : Type) (cT : type). -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class cT : class_of xT). - +Notation class := (class cT). (* Definition normedZmodType : normedZmodType cT := *) (* @NormedZmodule.Pack *) (* cT (Phant cT) cT *) -(* (NormedZmodule.Class (NumDomain.normed_mixin xclass)). *) +(* (NormedZmodule.Class (NumDomain.normed_mixin class)). *) Notation normedZmodType := (NormedZmodule.numDomain_normedZmodType cT). Definition normedZmod_ringType := - @GRing.Ring.Pack normedZmodType xclass. + @GRing.Ring.Pack normedZmodType class. Definition normedZmod_comRingType := - @GRing.ComRing.Pack normedZmodType xclass. + @GRing.ComRing.Pack normedZmodType class. Definition normedZmod_unitRingType := - @GRing.UnitRing.Pack normedZmodType xclass. + @GRing.UnitRing.Pack normedZmodType class. Definition normedZmod_comUnitRingType := - @GRing.ComUnitRing.Pack normedZmodType xclass. + @GRing.ComUnitRing.Pack normedZmodType class. Definition normedZmod_idomainType := - @GRing.IntegralDomain.Pack normedZmodType xclass. + @GRing.IntegralDomain.Pack normedZmodType class. Definition normedZmod_porderType := - @Order.POrder.Pack ring_display normedZmodType xclass. + @Order.POrder.Pack ring_display normedZmodType class. End NumDomain_joins. @@ -528,10 +526,12 @@ Module NumField. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : NumDomain.class_of R; mixin : GRing.Field.mixin_of (num_for R base); }. +Unset Primitive Projections. Local Coercion base : class_of >-> NumDomain.class_of. Local Coercion base2 R (c : class_of R) : GRing.Field.class_of _ := GRing.Field.Class (@mixin _ c). @@ -540,29 +540,26 @@ 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. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (NumDomain.class bT) (b : NumDomain.class_of T) => fun mT m & phant_id (GRing.Field.mixin (GRing.Field.class mT)) 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 porderType := @Order.POrder.Pack ring_display cT xclass. -Definition numDomainType := @NumDomain.Pack cT xclass. -Definition fieldType := @GRing.Field.Pack cT xclass. -Definition normedZmodType := NormedZmodType numDomainType cT xclass. -Definition porder_fieldType := @GRing.Field.Pack porderType xclass. -Definition normedZmod_fieldType := - @GRing.Field.Pack normedZmodType xclass. -Definition numDomain_fieldType := @GRing.Field.Pack numDomainType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition porderType := @Order.POrder.Pack ring_display cT class. +Definition numDomainType := @NumDomain.Pack cT class. +Definition fieldType := @GRing.Field.Pack cT class. +Definition normedZmodType := NormedZmodType numDomainType cT class. +Definition porder_fieldType := @GRing.Field.Pack porderType class. +Definition normedZmod_fieldType := @GRing.Field.Pack normedZmodType class. +Definition numDomain_fieldType := @GRing.Field.Pack numDomainType class. End ClassDef. @@ -617,12 +614,14 @@ Record imaginary_mixin_of (R : numDomainType) := ImaginaryMixin { _ : forall x, x * conj_op x = `|x| ^+ 2; }. +Set Primitive Projections. Record class_of R := Class { base : NumField.class_of R; decField_mixin : GRing.DecidableField.mixin_of (num_for R base); closedField_axiom : GRing.ClosedField.axiom (num_for R base); conj_mixin : imaginary_mixin_of (num_for R base); }. +Unset Primitive Projections. Local Coercion base : class_of >-> NumField.class_of. Local Coercion base2 R (c : class_of R) : GRing.ClosedField.class_of R := @GRing.ClosedField.Class @@ -633,8 +632,6 @@ 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. -Notation xclass := (class : class_of xT). Definition clone := fun b & phant_id class (b : class_of T) => Pack b. Definition pack := fun bT b & phant_id (NumField.class bT) (b : NumField.class_of T) => @@ -644,35 +641,35 @@ Definition pack := _ (@GRing.DecidableField.Class _ b dec) closed) => fun mc => Pack (@Class T b dec closed mc). -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 porderType := @Order.POrder.Pack ring_display 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 normedZmodType := NormedZmodType numDomainType cT xclass. -Definition porder_decFieldType := @GRing.DecidableField.Pack porderType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition porderType := @Order.POrder.Pack ring_display cT class. +Definition numDomainType := @NumDomain.Pack cT class. +Definition fieldType := @GRing.Field.Pack cT class. +Definition numFieldType := @NumField.Pack cT class. +Definition decFieldType := @GRing.DecidableField.Pack cT class. +Definition closedFieldType := @GRing.ClosedField.Pack cT class. +Definition normedZmodType := NormedZmodType numDomainType cT class. +Definition porder_decFieldType := @GRing.DecidableField.Pack porderType class. Definition normedZmod_decFieldType := - @GRing.DecidableField.Pack normedZmodType xclass. + @GRing.DecidableField.Pack normedZmodType class. Definition numDomain_decFieldType := - @GRing.DecidableField.Pack numDomainType xclass. + @GRing.DecidableField.Pack numDomainType class. Definition numField_decFieldType := - @GRing.DecidableField.Pack numFieldType xclass. -Definition porder_closedFieldType := @GRing.ClosedField.Pack porderType xclass. + @GRing.DecidableField.Pack numFieldType class. +Definition porder_closedFieldType := @GRing.ClosedField.Pack porderType class. Definition normedZmod_closedFieldType := - @GRing.ClosedField.Pack normedZmodType xclass. + @GRing.ClosedField.Pack normedZmodType class. Definition numDomain_closedFieldType := - @GRing.ClosedField.Pack numDomainType xclass. + @GRing.ClosedField.Pack numDomainType class. Definition numField_closedFieldType := - @GRing.ClosedField.Pack numFieldType xclass. + @GRing.ClosedField.Pack numFieldType class. End ClassDef. @@ -735,12 +732,14 @@ Module RealDomain. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : NumDomain.class_of R; nmixin : Order.Lattice.mixin_of base; lmixin : Order.DistrLattice.mixin_of (Order.Lattice.Class nmixin); tmixin : Order.Total.mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> NumDomain.class_of. Local Coercion base2 T (c : class_of T) : Order.Total.class_of T := @Order.Total.Class _ (@Order.DistrLattice.Class _ _ (lmixin c)) (@tmixin _ c). @@ -749,8 +748,6 @@ 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. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (NumDomain.class bT) (b : NumDomain.class_of T) => fun mT n l m & @@ -759,64 +756,64 @@ Definition pack := T (@Order.Lattice.Class T b n) l) m) => Pack (@Class T b n l 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 porderType := @Order.POrder.Pack ring_display cT xclass. -Definition latticeType := @Order.Lattice.Pack ring_display cT xclass. -Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass. -Definition orderType := @Order.Total.Pack ring_display cT xclass. -Definition numDomainType := @NumDomain.Pack cT xclass. -Definition normedZmodType := NormedZmodType numDomainType cT xclass. -Definition zmod_latticeType := @Order.Lattice.Pack ring_display zmodType xclass. -Definition ring_latticeType := @Order.Lattice.Pack ring_display ringType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition porderType := @Order.POrder.Pack ring_display cT class. +Definition latticeType := @Order.Lattice.Pack ring_display cT class. +Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT class. +Definition orderType := @Order.Total.Pack ring_display cT class. +Definition numDomainType := @NumDomain.Pack cT class. +Definition normedZmodType := NormedZmodType numDomainType cT class. +Definition zmod_latticeType := @Order.Lattice.Pack ring_display zmodType class. +Definition ring_latticeType := @Order.Lattice.Pack ring_display ringType class. Definition comRing_latticeType := - @Order.Lattice.Pack ring_display comRingType xclass. + @Order.Lattice.Pack ring_display comRingType class. Definition unitRing_latticeType := - @Order.Lattice.Pack ring_display unitRingType xclass. + @Order.Lattice.Pack ring_display unitRingType class. Definition comUnitRing_latticeType := - @Order.Lattice.Pack ring_display comUnitRingType xclass. + @Order.Lattice.Pack ring_display comUnitRingType class. Definition idomain_latticeType := - @Order.Lattice.Pack ring_display idomainType xclass. + @Order.Lattice.Pack ring_display idomainType class. Definition normedZmod_latticeType := - @Order.Lattice.Pack ring_display normedZmodType xclass. + @Order.Lattice.Pack ring_display normedZmodType class. Definition numDomain_latticeType := - @Order.Lattice.Pack ring_display numDomainType xclass. + @Order.Lattice.Pack ring_display numDomainType class. Definition zmod_distrLatticeType := - @Order.DistrLattice.Pack ring_display zmodType xclass. + @Order.DistrLattice.Pack ring_display zmodType class. Definition ring_distrLatticeType := - @Order.DistrLattice.Pack ring_display ringType xclass. + @Order.DistrLattice.Pack ring_display ringType class. Definition comRing_distrLatticeType := - @Order.DistrLattice.Pack ring_display comRingType xclass. + @Order.DistrLattice.Pack ring_display comRingType class. Definition unitRing_distrLatticeType := - @Order.DistrLattice.Pack ring_display unitRingType xclass. + @Order.DistrLattice.Pack ring_display unitRingType class. Definition comUnitRing_distrLatticeType := - @Order.DistrLattice.Pack ring_display comUnitRingType xclass. + @Order.DistrLattice.Pack ring_display comUnitRingType class. Definition idomain_distrLatticeType := - @Order.DistrLattice.Pack ring_display idomainType xclass. + @Order.DistrLattice.Pack ring_display idomainType class. Definition normedZmod_distrLatticeType := - @Order.DistrLattice.Pack ring_display normedZmodType xclass. + @Order.DistrLattice.Pack ring_display normedZmodType class. Definition numDomain_distrLatticeType := - @Order.DistrLattice.Pack ring_display numDomainType xclass. -Definition zmod_orderType := @Order.Total.Pack ring_display zmodType xclass. -Definition ring_orderType := @Order.Total.Pack ring_display ringType xclass. + @Order.DistrLattice.Pack ring_display numDomainType class. +Definition zmod_orderType := @Order.Total.Pack ring_display zmodType class. +Definition ring_orderType := @Order.Total.Pack ring_display ringType class. Definition comRing_orderType := - @Order.Total.Pack ring_display comRingType xclass. + @Order.Total.Pack ring_display comRingType class. Definition unitRing_orderType := - @Order.Total.Pack ring_display unitRingType xclass. + @Order.Total.Pack ring_display unitRingType class. Definition comUnitRing_orderType := - @Order.Total.Pack ring_display comUnitRingType xclass. + @Order.Total.Pack ring_display comUnitRingType class. Definition idomain_orderType := - @Order.Total.Pack ring_display idomainType xclass. + @Order.Total.Pack ring_display idomainType class. Definition normedZmod_orderType := - @Order.Total.Pack ring_display normedZmodType xclass. + @Order.Total.Pack ring_display normedZmodType class. Definition numDomain_orderType := - @Order.Total.Pack ring_display numDomainType xclass. + @Order.Total.Pack ring_display numDomainType class. End ClassDef. @@ -889,12 +886,14 @@ Module RealField. Section ClassDef. +Set Primitive Projections. Record class_of R := Class { base : NumField.class_of R; nmixin : Order.Lattice.mixin_of base; lmixin : Order.DistrLattice.mixin_of (Order.Lattice.Class nmixin); tmixin : Order.Total.mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> NumField.class_of. Local Coercion base2 R (c : class_of R) : RealDomain.class_of R := @RealDomain.Class _ _ (nmixin c) (lmixin c) (@tmixin R c). @@ -903,44 +902,42 @@ 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. -Notation xclass := (class : class_of xT). Definition pack := fun bT (b : NumField.class_of T) & phant_id (NumField.class bT) b => fun mT n l t & phant_id (RealDomain.class mT) (@RealDomain.Class T b n l t) => Pack (@Class T b n l t). -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 porderType := @Order.POrder.Pack ring_display cT xclass. -Definition numDomainType := @NumDomain.Pack cT xclass. -Definition latticeType := @Order.Lattice.Pack ring_display cT xclass. -Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass. -Definition orderType := @Order.Total.Pack ring_display cT xclass. -Definition realDomainType := @RealDomain.Pack cT xclass. -Definition fieldType := @GRing.Field.Pack cT xclass. -Definition numFieldType := @NumField.Pack cT xclass. -Definition normedZmodType := NormedZmodType numDomainType cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition porderType := @Order.POrder.Pack ring_display cT class. +Definition numDomainType := @NumDomain.Pack cT class. +Definition latticeType := @Order.Lattice.Pack ring_display cT class. +Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT class. +Definition orderType := @Order.Total.Pack ring_display cT class. +Definition realDomainType := @RealDomain.Pack cT class. +Definition fieldType := @GRing.Field.Pack cT class. +Definition numFieldType := @NumField.Pack cT class. +Definition normedZmodType := NormedZmodType numDomainType cT class. Definition field_latticeType := - @Order.Lattice.Pack ring_display fieldType xclass. + @Order.Lattice.Pack ring_display fieldType class. Definition field_distrLatticeType := - @Order.DistrLattice.Pack ring_display fieldType xclass. -Definition field_orderType := @Order.Total.Pack ring_display fieldType xclass. -Definition field_realDomainType := @RealDomain.Pack fieldType xclass. + @Order.DistrLattice.Pack ring_display fieldType class. +Definition field_orderType := @Order.Total.Pack ring_display fieldType class. +Definition field_realDomainType := @RealDomain.Pack fieldType class. Definition numField_latticeType := - @Order.Lattice.Pack ring_display numFieldType xclass. + @Order.Lattice.Pack ring_display numFieldType class. Definition numField_distrLatticeType := - @Order.DistrLattice.Pack ring_display numFieldType xclass. + @Order.DistrLattice.Pack ring_display numFieldType class. Definition numField_orderType := - @Order.Total.Pack ring_display numFieldType xclass. -Definition numField_realDomainType := @RealDomain.Pack numFieldType xclass. + @Order.Total.Pack ring_display numFieldType class. +Definition numField_realDomainType := @RealDomain.Pack numFieldType class. End ClassDef. @@ -1003,39 +1000,41 @@ Module ArchimedeanField. Section ClassDef. -Record class_of R := - Class { base : RealField.class_of R; _ : archimedean_axiom (num_for R base) }. +Set Primitive Projections. +Record class_of R := Class { + base : RealField.class_of R; + mixin : archimedean_axiom (num_for R base) +}. +Unset Primitive Projections. Local Coercion base : class_of >-> RealField.class_of. 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. -Notation xclass := (class : class_of xT). 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). -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 porderType := @Order.POrder.Pack ring_display cT xclass. -Definition latticeType := @Order.Lattice.Pack ring_display cT xclass. -Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass. -Definition orderType := @Order.Total.Pack ring_display 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. -Definition normedZmodType := NormedZmodType numDomainType cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition porderType := @Order.POrder.Pack ring_display cT class. +Definition latticeType := @Order.Lattice.Pack ring_display cT class. +Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT class. +Definition orderType := @Order.Total.Pack ring_display cT class. +Definition numDomainType := @NumDomain.Pack cT class. +Definition realDomainType := @RealDomain.Pack cT class. +Definition fieldType := @GRing.Field.Pack cT class. +Definition numFieldType := @NumField.Pack cT class. +Definition realFieldType := @RealField.Pack cT class. +Definition normedZmodType := NormedZmodType numDomainType cT class. End ClassDef. @@ -1094,39 +1093,41 @@ Module RealClosedField. Section ClassDef. -Record class_of R := - Class { base : RealField.class_of R; _ : real_closed_axiom (num_for R base) }. +Set Primitive Projections. +Record class_of R := Class { + base : RealField.class_of R; + mixin : real_closed_axiom (num_for R base) +}. +Unset Primitive Projections. Local Coercion base : class_of >-> RealField.class_of. 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. -Notation xclass := (class : class_of xT). 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). -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 porderType := @Order.POrder.Pack ring_display cT xclass. -Definition latticeType := @Order.Lattice.Pack ring_display cT xclass. -Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass. -Definition orderType := @Order.Total.Pack ring_display 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. -Definition normedZmodType := NormedZmodType numDomainType cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition comRingType := @GRing.ComRing.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class. +Definition idomainType := @GRing.IntegralDomain.Pack cT class. +Definition porderType := @Order.POrder.Pack ring_display cT class. +Definition latticeType := @Order.Lattice.Pack ring_display cT class. +Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT class. +Definition orderType := @Order.Total.Pack ring_display cT class. +Definition numDomainType := @NumDomain.Pack cT class. +Definition realDomainType := @RealDomain.Pack cT class. +Definition fieldType := @GRing.Field.Pack cT class. +Definition numFieldType := @NumField.Pack cT class. +Definition realFieldType := @RealField.Pack cT class. +Definition normedZmodType := NormedZmodType numDomainType cT class. End ClassDef. diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 839efa7..21394bd 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -113,10 +113,12 @@ Definition axiom_def n (V : lmodType R) of phant V := Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V). -Structure class_of V := Class { +Set Primitive Projections. +Record class_of V := Class { base : GRing.Lmodule.class_of R V; mixin : mixin_of (GRing.Lmodule.Pack _ base) }. +Unset Primitive Projections. Local Coercion base : class_of >-> GRing.Lmodule.class_of. Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. @@ -124,18 +126,16 @@ 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. -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)) := fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b => fun m & phant_id m0 m => Pack phR (@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 eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition lmodType := @GRing.Lmodule.Pack R phR cT class. End ClassDef. Notation axiom n V := (axiom_def n (Phant V)). diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 2a8dddc..bdff38a 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -125,10 +125,12 @@ Section ClassDef. Variable R : ringType. Implicit Type phR : phant R. +Set Primitive Projections. Record class_of A := Class { base1 : GRing.UnitAlgebra.class_of R A; mixin : Vector.mixin_of (GRing.Lmodule.Pack _ base1) }. +Unset Primitive Projections. 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. @@ -138,8 +140,6 @@ 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. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@GRing.UnitAlgebra.class R phR bT) @@ -147,21 +147,21 @@ Definition pack := fun mT m & phant_id (@Vector.class R phR mT) (@Vector.Class R T b m) => 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. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @GRing.Zmodule.Pack cT class. +Definition lmodType := @GRing.Lmodule.Pack R phR cT class. +Definition ringType := @GRing.Ring.Pack cT class. +Definition unitRingType := @GRing.UnitRing.Pack cT class. +Definition lalgType := @GRing.Lalgebra.Pack R phR cT class. +Definition algType := @GRing.Algebra.Pack R phR cT class. +Definition unitAlgType := @GRing.UnitAlgebra.Pack R phR cT class. +Definition vectType := @Vector.Pack R phR cT class. +Definition vect_ringType := @GRing.Ring.Pack vectType class. +Definition vect_unitRingType := @GRing.UnitRing.Pack vectType class. +Definition vect_lalgType := @GRing.Lalgebra.Pack R phR vectType class. +Definition vect_algType := @GRing.Algebra.Pack R phR vectType class. +Definition vect_unitAlgType := @GRing.UnitAlgebra.Pack R phR vectType class. End ClassDef. diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 69c1bb7..df7ef5a 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -93,12 +93,14 @@ Section FieldExt. Variable R : ringType. +Set Primitive Projections. Record class_of T := Class { base : Falgebra.class_of R T; comm_ext : commutative (Ring.mul base); idomain_ext : IntegralDomain.axiom (Ring.Pack base); field_ext : Field.mixin_of (UnitRing.Pack base) }. +Unset Primitive Projections. Local Coercion base : class_of >-> Falgebra.class_of. @@ -123,8 +125,6 @@ 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. -Notation xclass := (class : class_of xT). Definition pack := fun (bT : Falgebra.type phR) b @@ -142,55 +142,55 @@ Definition pack_eta K := 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). -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 comAlgType := @ComAlgebra.Pack R phR cT xclass. -Definition comUnitAlgType := @ComUnitAlgebra.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_comAlgType := @ComAlgebra.Pack R phR FalgType xclass. -Definition Falg_comUnitAlgType := @ComUnitAlgebra.Pack R phR 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_comAlgType := @ComAlgebra.Pack R phR vectType xclass. -Definition vect_comUnitAlgType := @ComUnitAlgebra.Pack R phR vectType xclass. -Definition vect_idomainType := @IntegralDomain.Pack vectType xclass. -Definition vect_fieldType := @Field.Pack vectType xclass. - -Definition comUnitAlg_idomainType := @IntegralDomain.Pack comUnitAlgType xclass. -Definition comUnitAlg_fieldType := @Field.Pack comUnitAlgType xclass. - -Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass. -Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass. - -Definition comAlg_idomainType := @IntegralDomain.Pack comAlgType xclass. -Definition comAlg_fieldType := @Field.Pack comAlgType xclass. - -Definition alg_idomainType := @IntegralDomain.Pack algType xclass. -Definition alg_fieldType := @Field.Pack algType xclass. - -Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass. -Definition lalg_fieldType := @Field.Pack lalgType xclass. - -Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass. -Definition lmod_fieldType := @Field.Pack lmodType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition unitRingType := @UnitRing.Pack cT class. +Definition comRingType := @ComRing.Pack cT class. +Definition comUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @IntegralDomain.Pack cT class. +Definition fieldType := @Field.Pack cT class. +Definition lmodType := @Lmodule.Pack R phR cT class. +Definition lalgType := @Lalgebra.Pack R phR cT class. +Definition algType := @Algebra.Pack R phR cT class. +Definition unitAlgType := @UnitAlgebra.Pack R phR cT class. +Definition comAlgType := @ComAlgebra.Pack R phR cT class. +Definition comUnitAlgType := @ComUnitAlgebra.Pack R phR cT class. +Definition vectType := @Vector.Pack R phR cT class. +Definition FalgType := @Falgebra.Pack R phR cT class. + +Definition Falg_comRingType := @ComRing.Pack FalgType class. +Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType class. +Definition Falg_comAlgType := @ComAlgebra.Pack R phR FalgType class. +Definition Falg_comUnitAlgType := @ComUnitAlgebra.Pack R phR FalgType class. +Definition Falg_idomainType := @IntegralDomain.Pack FalgType class. +Definition Falg_fieldType := @Field.Pack FalgType class. + +Definition vect_comRingType := @ComRing.Pack vectType class. +Definition vect_comUnitRingType := @ComUnitRing.Pack vectType class. +Definition vect_comAlgType := @ComAlgebra.Pack R phR vectType class. +Definition vect_comUnitAlgType := @ComUnitAlgebra.Pack R phR vectType class. +Definition vect_idomainType := @IntegralDomain.Pack vectType class. +Definition vect_fieldType := @Field.Pack vectType class. + +Definition comUnitAlg_idomainType := @IntegralDomain.Pack comUnitAlgType class. +Definition comUnitAlg_fieldType := @Field.Pack comUnitAlgType class. + +Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType class. +Definition unitAlg_fieldType := @Field.Pack unitAlgType class. + +Definition comAlg_idomainType := @IntegralDomain.Pack comAlgType class. +Definition comAlg_fieldType := @Field.Pack comAlgType class. + +Definition alg_idomainType := @IntegralDomain.Pack algType class. +Definition alg_fieldType := @Field.Pack algType class. + +Definition lalg_idomainType := @IntegralDomain.Pack lalgType class. +Definition lalg_fieldType := @Field.Pack lalgType class. + +Definition lmod_idomainType := @IntegralDomain.Pack lmodType class. +Definition lmod_fieldType := @Field.Pack lmodType class. End FieldExt. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index bbd6358..82c4819 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -340,16 +340,16 @@ Variable F : fieldType. Definition axiom (L : fieldExtType F) := exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}. +Set Primitive Projections. Record class_of (L : Type) : Type := - Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base)}. + Class {base : FieldExt.class_of F L; mixin : axiom (FieldExt.Pack _ base)}. +Unset Primitive Projections. Local Coercion base : class_of >-> FieldExt.class_of. 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. -Notation xclass := (class : class_of xT). Definition clone c of phant_id class c := @Pack phF T c. @@ -357,24 +357,24 @@ 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). -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 comAlgType := @ComAlgebra.Pack F phF cT xclass. -Definition comUnitAlgType := @ComUnitAlgebra.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. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition zmodType := @Zmodule.Pack cT class. +Definition ringType := @Ring.Pack cT class. +Definition unitRingType := @UnitRing.Pack cT class. +Definition comRingType := @ComRing.Pack cT class. +Definition comUnitRingType := @ComUnitRing.Pack cT class. +Definition idomainType := @IntegralDomain.Pack cT class. +Definition fieldType := @Field.Pack cT class. +Definition lmodType := @Lmodule.Pack F phF cT class. +Definition lalgType := @Lalgebra.Pack F phF cT class. +Definition algType := @Algebra.Pack F phF cT class. +Definition unitAlgType := @UnitAlgebra.Pack F phF cT class. +Definition comAlgType := @ComAlgebra.Pack F phF cT class. +Definition comUnitAlgType := @ComUnitAlgebra.Pack F phF cT class. +Definition vectType := @Vector.Pack F phF cT class. +Definition FalgType := @Falgebra.Pack F phF cT class. +Definition fieldExtType := @FieldExt.Pack F phF cT class. End ClassDef. diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index c065cd6..a68ec41 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -254,7 +254,9 @@ Record mixin_of T := Mixin { _ : forall P Q : pred T, P =1 Q -> find P =1 find Q }. +Set Primitive Projections. Record class_of T := Class {base : Equality.class_of T; mixin : mixin_of T}. +Unset Primitive Projections. Local Coercion base : class_of >-> Equality.class_of. Structure type := Pack {sort; _ : class_of sort}. @@ -262,14 +264,12 @@ 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. -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). (* Inheritance *) -Definition eqType := @Equality.Pack cT xclass. +Definition eqType := @Equality.Pack cT class. End ClassDef. @@ -523,7 +523,9 @@ Definition ChoiceMixin T m := PcanChoiceMixin (@pickleK T m). Section ClassDef. +Set Primitive Projections. Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }. +Unset Primitive Projections. Local Coercion base : class_of >-> Choice.class_of. Structure type : Type := Pack {sort : Type; _ : class_of sort}. @@ -531,14 +533,12 @@ 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. -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). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. End ClassDef. diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 7d65f9e..870b797 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -204,10 +204,12 @@ End Mixins. Section ClassDef. +Set Primitive Projections. Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of (Equality.Pack base) }. +Unset Primitive Projections. Definition base2 T c := Countable.Class (@base T c) (mixin_base (mixin c)). Local Coercion base : class_of >-> Choice.class_of. @@ -216,16 +218,14 @@ 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. -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). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition countType := @Countable.Pack cT (base2 xclass). +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT (base2 class). End ClassDef. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index e4b956d..b9ed011 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -1002,10 +1002,12 @@ Record mixin_of (T0 : Type) (b : Equality.class_of T0) _ : transitive le; }. +Set Primitive Projections. Record class_of (T : Type) := Class { base : Choice.class_of T; mixin : mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> Choice.class_of. @@ -1018,15 +1020,13 @@ Variables (T : Type) (disp : unit) (cT : type disp). Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Definition clone c of phant_id class c := @Pack disp T c. Definition clone_with disp' c of phant_id class c := @Pack disp' T c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (Choice.class bT) b => fun m => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. End ClassDef. Module Exports. @@ -1230,10 +1230,12 @@ Record mixin_of (T0 : Type) (b : POrder.class_of T0) _ : forall x y, (x <= y) = (meet x y == x); }. +Set Primitive Projections. Record class_of (T : Type) := Class { base : POrder.class_of T; mixin : mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> POrder.class_of. @@ -1246,16 +1248,14 @@ Variables (T : Type) (disp : unit) (cT : type disp). Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Definition clone c of phant_id class c := @Pack disp T c. Definition clone_with disp' c of phant_id class c := @Pack disp' T c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@POrder.class disp bT) b => fun m => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. End ClassDef. Module Exports. @@ -1341,10 +1341,12 @@ Record mixin_of (T : Type) (b : POrder.class_of T) _ : forall x, bottom <= x; }. +Set Primitive Projections. Record class_of (T : Type) := Class { base : Lattice.class_of T; mixin : mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> Lattice.class_of. @@ -1357,17 +1359,15 @@ Variables (T : Type) (disp : unit) (cT : type disp). Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Definition clone c of phant_id class c := @Pack disp T c. Definition clone_with disp' c of phant_id class c := @Pack disp' T c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@Lattice.class disp bT) b => fun m => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. End ClassDef. Module Exports. @@ -1444,10 +1444,12 @@ Record mixin_of (T0 : Type) (b : POrder.class_of T0) _ : forall x, x <= top; }. +Set Primitive Projections. Record class_of (T : Type) := Class { base : BLattice.class_of T; mixin : mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> BLattice.class_of. @@ -1460,18 +1462,16 @@ Variables (T : Type) (disp : unit) (cT : type disp). Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Definition clone c of phant_id class c := @Pack disp T c. Definition clone_with disp' c of phant_id class c := @Pack disp' T c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@BLattice.class disp bT) b => fun m => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition bLatticeType := @BLattice.Pack disp cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition bLatticeType := @BLattice.Pack disp cT class. End ClassDef. Module Exports. @@ -1548,10 +1548,12 @@ Record mixin_of (T0 : Type) (b : Lattice.class_of T0) _ : @left_distributive T T meet join; }. +Set Primitive Projections. Record class_of (T : Type) := Class { base : Lattice.class_of T; mixin : mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> Lattice.class_of. @@ -1564,17 +1566,15 @@ Variables (T : Type) (disp : unit) (cT : type disp). Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Definition clone c of phant_id class c := @Pack disp T c. Definition clone_with disp' c of phant_id class c := @Pack disp' T c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@Lattice.class disp bT) b => fun m => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. End ClassDef. Module Exports. @@ -1613,10 +1613,12 @@ Export DistrLattice.Exports. Module BDistrLattice. Section ClassDef. +Set Primitive Projections. Record class_of (T : Type) := Class { base : DistrLattice.class_of T; mixin : BLattice.mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> DistrLattice.class_of. Local Coercion base2 T (c : class_of T) : BLattice.class_of T := @@ -1629,21 +1631,19 @@ Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). 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 (@DistrLattice.class disp bT) b => fun mT m & phant_id (@BLattice.class disp mT) (BLattice.Class m) => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition bLatticeType := @BLattice.Pack disp cT xclass. -Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. -Definition nb_distrLatticeType := @DistrLattice.Pack disp bLatticeType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition bLatticeType := @BLattice.Pack disp cT class. +Definition distrLatticeType := @DistrLattice.Pack disp cT class. +Definition nb_distrLatticeType := @DistrLattice.Pack disp bLatticeType class. End ClassDef. Module Exports. @@ -1674,10 +1674,12 @@ Export BDistrLattice.Exports. Module TBDistrLattice. Section ClassDef. +Set Primitive Projections. Record class_of (T : Type) := Class { base : BDistrLattice.class_of T; mixin : TBLattice.mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> BDistrLattice.class_of. Local Coercion base2 T (c : class_of T) : TBLattice.class_of T := @@ -1690,8 +1692,6 @@ Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). 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 : BDistrLattice.class_of T) @@ -1699,17 +1699,17 @@ Definition pack := fun mT m & phant_id (@TBLattice.class disp mT) (@TBLattice.Class _ b m) => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition bLatticeType := @BLattice.Pack disp cT xclass. -Definition tbLatticeType := @TBLattice.Pack disp cT xclass. -Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. -Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. -Definition ntb_distrLatticeType := @DistrLattice.Pack disp tbLatticeType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition bLatticeType := @BLattice.Pack disp cT class. +Definition tbLatticeType := @TBLattice.Pack disp cT class. +Definition distrLatticeType := @DistrLattice.Pack disp cT class. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class. +Definition ntb_distrLatticeType := @DistrLattice.Pack disp tbLatticeType class. Definition ntb_bDistrLatticeType := - @BDistrLattice.Pack disp tbLatticeType xclass. + @BDistrLattice.Pack disp tbLatticeType class. End ClassDef. Module Exports. @@ -1752,10 +1752,12 @@ Record mixin_of (T0 : Type) (b : BDistrLattice.class_of T0) _ : forall x y, (x `&` y) `|` sub x y = x }. +Set Primitive Projections. Record class_of (T : Type) := Class { base : BDistrLattice.class_of T; mixin : mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> BDistrLattice.class_of. @@ -1768,20 +1770,18 @@ Variables (T : Type) (disp : unit) (cT : type disp). Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Definition clone c of phant_id class c := @Pack disp T c. Definition clone_with disp' c of phant_id class c := @Pack disp' T c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@BDistrLattice.class disp bT) b => fun m => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition bLatticeType := @BLattice.Pack disp cT xclass. -Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. -Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition bLatticeType := @BLattice.Pack disp cT class. +Definition distrLatticeType := @DistrLattice.Pack disp cT class. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class. End ClassDef. Module Exports. @@ -1839,11 +1839,13 @@ Record mixin_of (T0 : Type) (b : TBDistrLattice.class_of T0) _ : forall x, compl x = sub top x }. +Set Primitive Projections. Record class_of (T : Type) := Class { base : TBDistrLattice.class_of T; mixin1 : CBDistrLattice.mixin_of base; mixin2 : @mixin_of _ base (CBDistrLattice.sub mixin1); }. +Unset Primitive Projections. Local Coercion base : class_of >-> TBDistrLattice.class_of. Local Coercion base2 T (c : class_of T) : CBDistrLattice.class_of T := @@ -1858,27 +1860,25 @@ Variables (T : Type) (disp : unit) (cT : type disp). Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Definition clone c of phant_id class c := @Pack disp T c. Definition clone_with disp' c of phant_id class c := @Pack disp' T c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@TBDistrLattice.class disp bT) b => fun mT m0 & phant_id (@CBDistrLattice.class disp mT) (CBDistrLattice.Class m0) => fun m1 => Pack disp (@Class T b m0 m1). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition bLatticeType := @BLattice.Pack disp cT xclass. -Definition tbLatticeType := @TBLattice.Pack disp cT xclass. -Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. -Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. -Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass. -Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT xclass. -Definition cb_tbLatticeType := @TBLattice.Pack disp cbDistrLatticeType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition bLatticeType := @BLattice.Pack disp cT class. +Definition tbLatticeType := @TBLattice.Pack disp cT class. +Definition distrLatticeType := @DistrLattice.Pack disp cT class. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class. +Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT class. +Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT class. +Definition cb_tbLatticeType := @TBLattice.Pack disp cbDistrLatticeType class. Definition cb_tbDistrLatticeType := - @TBDistrLattice.Pack disp cbDistrLatticeType xclass. + @TBDistrLattice.Pack disp cbDistrLatticeType class. End ClassDef. Module Exports. @@ -1947,10 +1947,12 @@ Section ClassDef. Definition mixin_of T0 (b : POrder.class_of T0) (T := POrder.Pack tt b) := total (<=%O : rel T). +Set Primitive Projections. Record class_of (T : Type) := Class { base : DistrLattice.class_of T; mixin : mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> DistrLattice.class_of. @@ -1963,18 +1965,16 @@ Variables (T : Type) (disp : unit) (cT : type disp). Definition class := let: Pack _ c as cT' := cT return class_of cT' in c. Definition clone c & phant_id class c := @Pack disp T c. Definition clone_with disp' c & phant_id class c := @Pack disp' T c. -Let xT := let: Pack T _ := cT in T. -Notation xclass := (class : class_of xT). Definition pack := fun bT b & phant_id (@DistrLattice.class disp bT) b => fun m => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition distrLatticeType := @DistrLattice.Pack disp cT class. End ClassDef. @@ -2016,10 +2016,12 @@ Import Total.Exports. Module FinPOrder. Section ClassDef. +Set Primitive Projections. Record class_of (T : Type) := Class { base : POrder.class_of T; mixin : Finite.mixin_of (Equality.Pack base) }. +Unset Primitive Projections. Local Coercion base : class_of >-> POrder.class_of. Local Coercion base2 T (c : class_of T) : Finite.class_of T := @@ -2032,21 +2034,19 @@ Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). 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 (@POrder.class disp bT) b => fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition countType := @Countable.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition count_porderType := @POrder.Pack disp countType xclass. -Definition fin_porderType := @POrder.Pack disp finType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT class. +Definition finType := @Finite.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition count_porderType := @POrder.Pack disp countType class. +Definition fin_porderType := @POrder.Pack disp finType class. End ClassDef. Module Exports. @@ -2077,10 +2077,12 @@ Bind Scope cpo_sort with FinPOrder.sort. Module FinLattice. Section ClassDef. +Set Primitive Projections. Record class_of (T : Type) := Class { base : TBLattice.class_of T; mixin : Finite.mixin_of (Equality.Pack base); }. +Unset Primitive Projections. Local Coercion base : class_of >-> TBLattice.class_of. Local Coercion base2 T (c : class_of T) : FinPOrder.class_of T := @@ -2093,32 +2095,30 @@ Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). 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 (@TBLattice.class disp bT) b => fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition countType := @Countable.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition bLatticeType := @BLattice.Pack disp cT xclass. -Definition tbLatticeType := @TBLattice.Pack disp cT xclass. -Definition count_latticeType := @Lattice.Pack disp countType xclass. -Definition count_bLatticeType := @BLattice.Pack disp countType xclass. -Definition count_tbLatticeType := @TBLattice.Pack disp countType xclass. -Definition fin_latticeType := @Lattice.Pack disp finType xclass. -Definition fin_bLatticeType := @BLattice.Pack disp finType xclass. -Definition fin_tbLatticeType := @TBLattice.Pack disp finType xclass. -Definition finPOrder_latticeType := @Lattice.Pack disp finPOrderType xclass. -Definition finPOrder_bLatticeType := @BLattice.Pack disp finPOrderType xclass. -Definition finPOrder_tbLatticeType := @TBLattice.Pack disp finPOrderType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT class. +Definition finType := @Finite.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition finPOrderType := @FinPOrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition bLatticeType := @BLattice.Pack disp cT class. +Definition tbLatticeType := @TBLattice.Pack disp cT class. +Definition count_latticeType := @Lattice.Pack disp countType class. +Definition count_bLatticeType := @BLattice.Pack disp countType class. +Definition count_tbLatticeType := @TBLattice.Pack disp countType class. +Definition fin_latticeType := @Lattice.Pack disp finType class. +Definition fin_bLatticeType := @BLattice.Pack disp finType class. +Definition fin_tbLatticeType := @TBLattice.Pack disp finType class. +Definition finPOrder_latticeType := @Lattice.Pack disp finPOrderType class. +Definition finPOrder_bLatticeType := @BLattice.Pack disp finPOrderType class. +Definition finPOrder_tbLatticeType := @TBLattice.Pack disp finPOrderType class. End ClassDef. @@ -2164,10 +2164,12 @@ Export FinLattice.Exports. Module FinDistrLattice. Section ClassDef. +Set Primitive Projections. Record class_of (T : Type) := Class { base : TBDistrLattice.class_of T; mixin : Finite.mixin_of (Equality.Pack base); }. +Unset Primitive Projections. Local Coercion base : class_of >-> TBDistrLattice.class_of. Local Coercion base2 T (c : class_of T) : FinLattice.class_of T := @@ -2180,46 +2182,44 @@ Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). 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 (@TBDistrLattice.class disp bT) b => fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition countType := @Countable.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition bLatticeType := @BLattice.Pack disp cT xclass. -Definition tbLatticeType := @TBLattice.Pack disp cT xclass. -Definition finLatticeType := @FinLattice.Pack disp cT xclass. -Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. -Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. -Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass. -Definition count_distrLatticeType := @DistrLattice.Pack disp countType xclass. -Definition count_bDistrLatticeType := @BDistrLattice.Pack disp countType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT class. +Definition finType := @Finite.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition finPOrderType := @FinPOrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition bLatticeType := @BLattice.Pack disp cT class. +Definition tbLatticeType := @TBLattice.Pack disp cT class. +Definition finLatticeType := @FinLattice.Pack disp cT class. +Definition distrLatticeType := @DistrLattice.Pack disp cT class. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class. +Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT class. +Definition count_distrLatticeType := @DistrLattice.Pack disp countType class. +Definition count_bDistrLatticeType := @BDistrLattice.Pack disp countType class. Definition count_tbDistrLatticeType := - @TBDistrLattice.Pack disp countType xclass. -Definition fin_distrLatticeType := @DistrLattice.Pack disp finType xclass. -Definition fin_bDistrLatticeType := @BDistrLattice.Pack disp finType xclass. -Definition fin_tbDistrLatticeType := @TBDistrLattice.Pack disp finType xclass. + @TBDistrLattice.Pack disp countType class. +Definition fin_distrLatticeType := @DistrLattice.Pack disp finType class. +Definition fin_bDistrLatticeType := @BDistrLattice.Pack disp finType class. +Definition fin_tbDistrLatticeType := @TBDistrLattice.Pack disp finType class. Definition finPOrder_distrLatticeType := - @DistrLattice.Pack disp finPOrderType xclass. + @DistrLattice.Pack disp finPOrderType class. Definition finPOrder_bDistrLatticeType := - @BDistrLattice.Pack disp finPOrderType xclass. + @BDistrLattice.Pack disp finPOrderType class. Definition finPOrder_tbDistrLatticeType := - @TBDistrLattice.Pack disp finPOrderType xclass. + @TBDistrLattice.Pack disp finPOrderType class. Definition finLattice_distrLatticeType := - @DistrLattice.Pack disp finLatticeType xclass. + @DistrLattice.Pack disp finLatticeType class. Definition finLattice_bDistrLatticeType := - @BDistrLattice.Pack disp finLatticeType xclass. + @BDistrLattice.Pack disp finLatticeType class. Definition finLattice_tbDistrLatticeType := - @TBDistrLattice.Pack disp finLatticeType xclass. + @TBDistrLattice.Pack disp finLatticeType class. End ClassDef. @@ -2276,10 +2276,12 @@ Export FinDistrLattice.Exports. Module FinCDistrLattice. Section ClassDef. +Set Primitive Projections. Record class_of (T : Type) := Class { base : CTBDistrLattice.class_of T; mixin : Finite.mixin_of (Equality.Pack base); }. +Unset Primitive Projections. Local Coercion base : class_of >-> CTBDistrLattice.class_of. Local Coercion base2 T (c : class_of T) : FinDistrLattice.class_of T := @@ -2292,48 +2294,46 @@ Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). 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 (@CTBDistrLattice.class disp bT) b => fun mT m & phant_id (@Finite.class mT) (@Finite.Class _ _ m) => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition countType := @Countable.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition bLatticeType := @BLattice.Pack disp cT xclass. -Definition tbLatticeType := @TBLattice.Pack disp cT xclass. -Definition finLatticeType := @FinLattice.Pack disp cT xclass. -Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. -Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. -Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass. -Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT xclass. -Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT xclass. -Definition ctbDistrLatticeType := @CTBDistrLattice.Pack disp cT xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT class. +Definition finType := @Finite.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition finPOrderType := @FinPOrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition bLatticeType := @BLattice.Pack disp cT class. +Definition tbLatticeType := @TBLattice.Pack disp cT class. +Definition finLatticeType := @FinLattice.Pack disp cT class. +Definition distrLatticeType := @DistrLattice.Pack disp cT class. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class. +Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT class. +Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT class. +Definition cbDistrLatticeType := @CBDistrLattice.Pack disp cT class. +Definition ctbDistrLatticeType := @CTBDistrLattice.Pack disp cT class. Definition count_cbDistrLatticeType := - @CBDistrLattice.Pack disp countType xclass. + @CBDistrLattice.Pack disp countType class. Definition count_ctbDistrLatticeType := - @CTBDistrLattice.Pack disp countType xclass. -Definition fin_cbDistrLatticeType := @CBDistrLattice.Pack disp finType xclass. -Definition fin_ctbDistrLatticeType := @CTBDistrLattice.Pack disp finType xclass. + @CTBDistrLattice.Pack disp countType class. +Definition fin_cbDistrLatticeType := @CBDistrLattice.Pack disp finType class. +Definition fin_ctbDistrLatticeType := @CTBDistrLattice.Pack disp finType class. Definition finPOrder_cbDistrLatticeType := - @CBDistrLattice.Pack disp finPOrderType xclass. + @CBDistrLattice.Pack disp finPOrderType class. Definition finPOrder_ctbDistrLatticeType := - @CTBDistrLattice.Pack disp finPOrderType xclass. + @CTBDistrLattice.Pack disp finPOrderType class. Definition finLattice_cbDistrLatticeType := - @CBDistrLattice.Pack disp finLatticeType xclass. + @CBDistrLattice.Pack disp finLatticeType class. Definition finLattice_ctbDistrLatticeType := - @CTBDistrLattice.Pack disp finLatticeType xclass. + @CTBDistrLattice.Pack disp finLatticeType class. Definition finDistrLattice_cbDistrLatticeType := - @CBDistrLattice.Pack disp finDistrLatticeType xclass. + @CBDistrLattice.Pack disp finDistrLatticeType class. Definition finDistrLattice_ctbDistrLatticeType := - @CTBDistrLattice.Pack disp finDistrLatticeType xclass. + @CTBDistrLattice.Pack disp finDistrLatticeType class. End ClassDef. @@ -2394,10 +2394,12 @@ Export FinCDistrLattice.Exports. Module FinTotal. Section ClassDef. +Set Primitive Projections. Record class_of (T : Type) := Class { base : FinDistrLattice.class_of T; mixin : Total.mixin_of base; }. +Unset Primitive Projections. Local Coercion base : class_of >-> FinDistrLattice.class_of. Local Coercion base2 T (c : class_of T) : Total.class_of T := @@ -2410,40 +2412,38 @@ Local Coercion sort : type >-> Sortclass. Variables (T : Type) (disp : unit) (cT : type disp). 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 (@FinDistrLattice.class disp bT) b => fun mT m & phant_id (@Total.class disp mT) (Total.Class m) => Pack disp (@Class T b m). -Definition eqType := @Equality.Pack cT xclass. -Definition choiceType := @Choice.Pack cT xclass. -Definition countType := @Countable.Pack cT xclass. -Definition finType := @Finite.Pack cT xclass. -Definition porderType := @POrder.Pack disp cT xclass. -Definition finPOrderType := @FinPOrder.Pack disp cT xclass. -Definition latticeType := @Lattice.Pack disp cT xclass. -Definition bLatticeType := @BLattice.Pack disp cT xclass. -Definition tbLatticeType := @TBLattice.Pack disp cT xclass. -Definition finLatticeType := @FinLattice.Pack disp cT xclass. -Definition distrLatticeType := @DistrLattice.Pack disp cT xclass. -Definition bDistrLatticeType := @BDistrLattice.Pack disp cT xclass. -Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT xclass. -Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT xclass. -Definition orderType := @Total.Pack disp cT xclass. -Definition order_countType := @Countable.Pack orderType xclass. -Definition order_finType := @Finite.Pack orderType xclass. -Definition order_finPOrderType := @FinPOrder.Pack disp orderType xclass. -Definition order_bLatticeType := @BLattice.Pack disp orderType xclass. -Definition order_tbLatticeType := @TBLattice.Pack disp orderType xclass. -Definition order_finLatticeType := @FinLattice.Pack disp orderType xclass. -Definition order_bDistrLatticeType := @BDistrLattice.Pack disp orderType xclass. +Definition eqType := @Equality.Pack cT class. +Definition choiceType := @Choice.Pack cT class. +Definition countType := @Countable.Pack cT class. +Definition finType := @Finite.Pack cT class. +Definition porderType := @POrder.Pack disp cT class. +Definition finPOrderType := @FinPOrder.Pack disp cT class. +Definition latticeType := @Lattice.Pack disp cT class. +Definition bLatticeType := @BLattice.Pack disp cT class. +Definition tbLatticeType := @TBLattice.Pack disp cT class. +Definition finLatticeType := @FinLattice.Pack disp cT class. +Definition distrLatticeType := @DistrLattice.Pack disp cT class. +Definition bDistrLatticeType := @BDistrLattice.Pack disp cT class. +Definition tbDistrLatticeType := @TBDistrLattice.Pack disp cT class. +Definition finDistrLatticeType := @FinDistrLattice.Pack disp cT class. +Definition orderType := @Total.Pack disp cT class. +Definition order_countType := @Countable.Pack orderType class. +Definition order_finType := @Finite.Pack orderType class. +Definition order_finPOrderType := @FinPOrder.Pack disp orderType class. +Definition order_bLatticeType := @BLattice.Pack disp orderType class. +Definition order_tbLatticeType := @TBLattice.Pack disp orderType class. +Definition order_finLatticeType := @FinLattice.Pack disp orderType class. +Definition order_bDistrLatticeType := @BDistrLattice.Pack disp orderType class. Definition order_tbDistrLatticeType := - @TBDistrLattice.Pack disp orderType xclass. + @TBDistrLattice.Pack disp orderType class. Definition order_finDistrLatticeType := - @FinDistrLattice.Pack disp orderType xclass. + @FinDistrLattice.Pack disp orderType class. End ClassDef. diff --git a/mathcomp/test_suite/test_regular_conv.v b/mathcomp/test_suite/test_regular_conv.v new file mode 100644 index 0000000..b6c9f05 --- /dev/null +++ b/mathcomp/test_suite/test_regular_conv.v @@ -0,0 +1,34 @@ +From mathcomp Require Import all_ssreflect all_algebra all_field. + +Section regular. + +Import GRing. + +Let eq_ringType_of_regular_lalgType (R : ringType) := + erefl : regular_lalgType R = Ring.Pack (Ring.class R) :> ringType. + +Let eq_ringType_of_regular_algType (R : comRingType) := + erefl : regular_algType R = Ring.Pack (Ring.class R) :> ringType. + +Let eq_comRingType_of_regular_comAlgType (R : comRingType) := + erefl : regular_comAlgType R = ComRing.Pack (ComRing.class R) :> ringType. + +Let eq_unitRingType_of_regular_unitAlgType (R : comUnitRingType) := + erefl : regular_unitAlgType R = + UnitRing.Pack (UnitRing.class R) :> unitRingType. + +(* The following assertion fails if the class records are not primitive *) +(* because the [comUnitAlgType _ of _] packager inserts an eta-expansion on *) +(* the class. *) +Let eq_comUnitRingType_of_regular_comUnitAlgType (R : comUnitRingType) := + erefl : regular_comUnitAlgType R = + ComUnitRing.Pack (ComUnitRing.class R) :> comUnitRingType. + +Let eq_unitRingType_of_regular_FalgType (R : comUnitRingType) := + erefl : regular_FalgType R = UnitRing.Pack (UnitRing.class R) :> unitRingType. + +(* The following assertion also fails if the class records are not primitive. *) +Let eq_fieldType_of_regular_fieldExtType (K : fieldType) := + erefl : regular_fieldExtType K = Field.Pack (Field.class K) :> fieldType. + +End regular. |