Stream: Hierarchy Builder devs & users

Topic: Success ! FormalPowerSeries for MathComp 2


view this post on Zulip Florent Hivert (Nov 27 2023 at 21:46):

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:

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 !

view this post on Zulip Cyril Cohen (Nov 28 2023 at 08:00):

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.

view this post on Zulip Florent Hivert (Nov 28 2023 at 08:08):

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

view this post on Zulip Kazuhiko Sakaguchi (Nov 28 2023 at 12:36):

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