Florent Hivert comments

Results 27 comments of


                                            Florent Hivert

Extending `rel` theory

I'm not sure what you have in mind but I wrote some quite advanced surgery on finite relations in the file https://github.com/hivert/Coq-Combi/blob/posets/theories/Poset/poset.v I would be glad if any of it...

Documentation of character.v

I'm ok to help here, I'm asking if it is left undocumented on purpose.

Documentation of character.v

There is also the question of naming convention: I thing that `prod_repr` should be `prod_grepr` for consistency with `muln_grepr`, `dadd_grepr` , `prod_repr`... Any agreement on that ?

Documentation of character.v

@ggonthier : Thanks for your detailed answer. I was suspecting that you didn't want to expose those construction, because while general, then were not sufficiently developed to be exposed. That's...

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

See https://github.com/math-comp/math-comp/pull/806 for a temporary fix that only correct the documentation.

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

@CohenCyril Sure ! I've got one question for you relevant to this issue: the first step of @ggonthier plan is to generalize group to infinite groups. That mean rewriting the...

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

Thanks for the answer. So I'm waiting to try to solve this issue.

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

@proux01: Sure. I'll probably need several step such as: - generalization of groups to infinite one - morphisms beetween infinite groups - do we want to generalize all the various...

Syntactic sugar \is and coercion

@ggonthier: thanks for the explanation. It is clear that the user expect that the matching selection mechanism works from left to right. So the order inversion would be surprising. So...

Syntactic sugar \is and coercion

I'm not sure to fully understand the request... So I'd rather have you take care of it.