Florent Hivert

In presentation.v G \isog Grp(...) doesn't really says that ... is a presentation of G.

7

The files presentation.v aims to define presentation of groups. However, since in MathComp, all the groups are assumed to be finite.What is defined here is something subtly different: The predicate...

Documentation of character.v

7

There are several definitions in `character.v` which are not documented: - `trow` and `trowb`,`tprod` : tensor (also called) Kronecker product of matrices - `grepr0` and `dadd_grepr` : nul and direct...

Mixin for lattice

5

Currently the mixin for lattice contains a lot of obligations (this is the algebraic point of view on lattices): ``` Record mixin_of (T0 : Type) (b : POrder.class_of T0) (T...

Extends the basic group theory to infinite group

1

Typical usage is the unit group of an infinite ring. I guess there is a good reason why it wasn't done that way in the first place. Please comment and...

Syntactic sugar \is and coercion

7

The syntactic sugars `a \is b` and `a \is a b` allow for very readable statement. However, they doesn't play nice with coercions: The following code works as expected: ```...

##### Motivation for this change The condition of the lemma `telescope_sumn_in` doesn't seems what was intended and is not the most general. Indeed the condition ``` {in [pred i |...

In the following code, HB takes nearly 30s to find the unit ring instance. Some variation are faster. I got something even much slower (more that 2 min) on more...

The following code ``` From HB Require Import structures. From mathcomp Require Import all_ssreflect. Structure foo : Type := Foo {fooval :> seq nat; _ : size fooval == 1}....

In the case of misspelling of the key such as in ``` #[key="Tmiss"] HB.mixin Record Foo T := {}. ``` I think HB should not stay silent.

Spurious warning `Projection value has no head constant`

1

Here is an example: ``` Variable R : ringType. Variable n : nat. Implicit Types (p q r s : {poly R}). Record truncfps := MkTfps { tfps : {poly...