Ssreflect Users Discussion List

[Xavier Allamigeon <>]

Dear Kazuhiko,

Thanks a lot to you and the MathComp team for these great news, the 
integration of the order library in MathComp will make our lives much 
easier.

Best,
Xavier

Le 22/02/2019 à 10:52, Kazuhiko Sakaguchi a écrit :
> Dear Xavier,
>
> I have good news for you and who interested in Cyril's order library.
>
> I'm have almost finished to port the order library into MathComp and
> reimplement the ssrnum structures (numDomainType, realDomainType,
> etc.) on top of the order structures.
> Currently, there is no standard implementation of "pointwise orders
> over matrices/vectors" and I'm not sure if our implementation is
> stable enough. However, it is easy to share the notion of order with
> various kind of ordered sets (ssrnum structures, matrices, intervals,
> etc.) and provide a latticeType instance of matrices. I hope it is
> really useful for someone...
>
> I'll be glad to answer any questions. More details can be found here:
> https://github.com/math-comp/math-comp/pull/270
>
> Best regards,
> Kazuhiko
>
> 2016年11月18日(金) 19:59 Xavier Allamigeon 
> <>:
> > Dear Cyril,
> >
> > Le 17/11/2016 à 13:03, Cyril a écrit :
> > > I am currently working on an order library
> > > https://github.com/Barbichu/finmap/blob/master/order.v
> > > Warning: draft version, work in progress, outdated header
> > >
> > > I hope to merge it with ssreflect one day.
> > Great, thanks for sharing this information. We would be glad to use it
> > once you consider that it is stable enough!
> >
> > Best,
> > Xavier