Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
After #743, there are 4 remarks remaining: #### finfun https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/ssreflect/finfun.v#L18-L21 We cannot address this right now (#701). #### ssralg https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/ssralg.v#L1856-L1858 https://github.com/math-comp/math-comp/blob/9bfc9834b46c1e492aaaf257cfa811d1e5e39065/mathcomp/algebra/ssralg.v#L3551-L3552 I didn't manage to understand what are the issues...
I unassign me since I don't see any immediate fix for the remaining ones. I think we need a volunteer to look at ssralg.
> *The first obstacle is that `falgebra.v` does not compile since both `prodv` and `capv` (`Order.meet`) distributes over `addv` (`Order.join`) and so `addv_addoid` (in `falgebra.v`) is now redundant with `join_addoid`...
> But, if there is a multiplication-like operator that distributes over two different addition-like operators, it does not work. I self answer this: `muln` distributes over `maxn` and `addn`, and...
The unification trace obtained by UniCoq (see https://github.com/math-comp/math-comp/issues/701#issuecomment-843729180 for the first attempt with `Set Debug "unification"`): https://github.com/math-comp/math-comp/blob/7db7a5fbce42ff387a5750f9fbde5436a9aab1cc/mathcomp/algebra/matrix.v#L342-L343 ``` eqType =
> Currently, `classfun.v` is broken since it uses `Cint`, but importing `ssrint` adds the infix `^` notation which collides with that of `group_scope`. It seems that group notations and ring...
I guess `Qint` and `Qnat` should be deprecated and superseded by `Cint` and `Cnat` respectively. Right? @CohenCyril
> > Yes! And `Cint` and `Cnat` should both be renamed `Num.int` and `Num.nat`. > > And they should be in the mixin, so as to make the computations for...
@CohenCyril Could you confirm this is what you mean? ```coq (* Module ArchiNumDomain. *) Record mixin_of (R : numDomainType) := Mixin { trunc : R -> nat; is_nat : pred...