diff options
Diffstat (limited to 'mathcomp/algebra/vector.v')
| -rw-r--r-- | mathcomp/algebra/vector.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 542f8ad..75b2073 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -117,27 +117,27 @@ Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V). Structure class_of V := Class { base : GRing.Lmodule.class_of R V; - mixin : mixin_of (GRing.Lmodule.Pack _ base V) + mixin : mixin_of (GRing.Lmodule.Pack _ base) }. Local Coercion base : class_of >-> GRing.Lmodule.class_of. -Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}. +Structure type (phR : phant R) := Pack {sort; _ : class_of sort}. Local Coercion sort : type >-> Sortclass. Variables (phR : phant R) (T : Type) (cT : type phR). -Definition class := let: Pack _ c _ := cT return class_of cT in c. -Definition clone c of phant_id class c := @Pack phR T c T. -Let xT := let: Pack T _ _ := cT in T. +Definition class := let: Pack _ c := cT return class_of cT in c. +Definition clone c of phant_id class c := @Pack phR T c. +Let xT := let: Pack T _ := cT in T. Notation xclass := (class : class_of xT). Definition dim := let: Mixin n _ := mixin class in n. -Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0 T)) := +Definition pack b0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ T b0)) := fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b => - fun m & phant_id m0 m => Pack phR (@Class T b m) T. + fun m & phant_id m0 m => Pack phR (@Class T b m). -Definition eqType := @Equality.Pack cT xclass xT. -Definition choiceType := @Choice.Pack cT xclass xT. -Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. -Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT. +Definition eqType := @Equality.Pack cT xclass. +Definition choiceType := @Choice.Pack cT xclass. +Definition zmodType := @GRing.Zmodule.Pack cT xclass. +Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass. End ClassDef. Notation axiom n V := (axiom_def n (Phant V)). |