I'm happy to report that I've successfully ported my development on formal power series to MathComp-2. It is currently available in a specific branch https://github.com/hivert/FormalPowerSeries/tree/mathcomp-2

It contains a formalization of the notion of inverse/co/projective limit and is therefore heavy on algebraic structure and hierarchy. So this provide a good use case to HB.

Some remarks:

- once one understand how it works, it is
**MUCH EASIER**to develop hierarchy using HB. Kudos for all of yours !!! - There are still a few side thing which need to be ported
- The fact that builder/stucture/... cannot be declared in a section leads to a lot of repetition in particular in the file invlim.v

Any idea on how to avoid that is welcome.

More generally, if some expert could have a look at what I wrote, that would be very helpful. In exchange, I'm offering to help for the user documentation of HB. Please tell me how I can help !

Hi @Florent Hivert if you make a PR from your mathcomp-2 branch onto master, it will display a diff and enable the review mode from github. I will give feedback then.

Hi @Cyril Cohen. This is https://github.com/hivert/FormalPowerSeries/pull/1

Thanks !

I will take a look mainly at `tfps.v`

(which is related to math-comp/math-comp#1128).

Last updated: Apr 21 2024 at 02:41 UTC