For example, the instances below seem redundant.
|
HB.instance Definition _ m n := SwizzleAdd (@trmx V m n). |
|
HB.instance Definition _ m n i := SwizzleAdd (@row V m n i). |
|
HB.instance Definition _ m n j := SwizzleAdd (@col V m n j). |
|
HB.instance Definition _ m n i := SwizzleAdd (@row' V m n i). |
|
HB.instance Definition _ m n j := SwizzleAdd (@col' V m n j). |
|
HB.instance Definition _ m n m' n' f g := SwizzleAdd (@mxsub V m n m' n' f g). |
|
HB.instance Definition _ m n s := SwizzleAdd (@row_perm V m n s). |
|
HB.instance Definition _ m n s := SwizzleAdd (@col_perm V m n s). |
|
HB.instance Definition _ m n i1 i2 := SwizzleAdd (@xrow V m n i1 i2). |
|
HB.instance Definition _ m n j1 j2 := SwizzleAdd (@xcol V m n j1 j2). |
|
HB.instance Definition _ m n1 n2 := SwizzleAdd (@lsubmx V m n1 n2). |
|
HB.instance Definition _ m n1 n2 := SwizzleAdd (@rsubmx V m n1 n2). |
|
HB.instance Definition _ m1 m2 n := SwizzleAdd (@usubmx V m1 m2 n). |
|
HB.instance Definition _ m1 m2 n := SwizzleAdd (@dsubmx V m1 m2 n). |
|
HB.instance Definition _ m n := SwizzleAdd (@vec_mx V m n). |
|
HB.instance Definition _ m n := GRing.isSemiAdditive.Build 'M_(m, n) 'rV_(m * n) |
|
mxvec (can2_semi_additive (@vec_mxK V m n) mxvecK). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n := SwizzleAdd (@trmx V m n). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n i := SwizzleAdd (@row V m n i). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n j := SwizzleAdd (@col V m n j). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n i := SwizzleAdd (@row' V m n i). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n j := SwizzleAdd (@col' V m n j). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n m' n' f g := SwizzleAdd (@mxsub V m n m' n' f g). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n s := SwizzleAdd (@row_perm V m n s). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n s := SwizzleAdd (@col_perm V m n s). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n i1 i2 := SwizzleAdd (@xrow V m n i1 i2). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n j1 j2 := SwizzleAdd (@xcol V m n j1 j2). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n1 n2 := SwizzleAdd (@lsubmx V m n1 n2). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n1 n2 := SwizzleAdd (@rsubmx V m n1 n2). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m1 m2 n := SwizzleAdd (@usubmx V m1 m2 n). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m1 m2 n := SwizzleAdd (@dsubmx V m1 m2 n). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n := SwizzleAdd (@vec_mx V m n). |
|
#[warning="-HB.no-new-instance"] |
|
HB.instance Definition _ m n := GRing.isAdditive.Build 'M_(m, n) 'rV_(m * n) |
|
mxvec (can2_additive (@vec_mxK V m n) mxvecK). |
I guess the particular instance of redundancy above was introduced because of the duplication of semi-additive and additive functions that happened while porting MC to HB (then removed before the release of MC 2.0).
I'm almost certain that all these instance declarations can be safely removed, but it would also involve the removal of internal lemmas. Such an extensive clean-up should probably be done after the release of 2.4.0.
For example, the instances below seem redundant.
math-comp/algebra/matrix.v
Lines 1664 to 1680 in a67482a
math-comp/algebra/matrix.v
Lines 2163 to 2195 in a67482a
I guess the particular instance of redundancy above was introduced because of the duplication of semi-additive and additive functions that happened while porting MC to HB (then removed before the release of MC 2.0).
I'm almost certain that all these instance declarations can be safely removed, but it would also involve the removal of internal lemmas. Such an extensive clean-up should probably be done after the release of 2.4.0.