Stream: math-comp users

Topic: finmap-order


view this post on Zulip Pierre-Yves Strub (Jun 02 2020 at 13:38):

Hi. Are finmaps equipped with a porder structure? Otherwise, I'll got for it.

view this post on Zulip Cyril Cohen (Jun 02 2020 at 15:34):

Pierre-Yves Strub said:

Hi. Are finmaps equipped with a porder structure? Otherwise, I'll got for it.

I do not think they are... Is there even a canonical choice? (in case the keys differ)

view this post on Zulip Pierre-Yves Strub (Jun 02 2020 at 15:44):

finset :)

view this post on Zulip Cyril Cohen (Jun 02 2020 at 16:37):

ah! oh! I see, then, this was the ultimate goal of https://github.com/math-comp/finmap/blob/master/set.v ...

view this post on Zulip Cyril Cohen (Jun 02 2020 at 16:38):

provide a full set abstraction on top of order.v and rely on canonical generic set operations for all kinds of finite, co-finite, mixed-finite-co-finite and algebraic sets altogether

view this post on Zulip Cyril Cohen (Jun 02 2020 at 16:39):

and intervals

view this post on Zulip Cyril Cohen (Jun 02 2020 at 16:40):

This grew out of hand, and I expect to resume as soon as HB + parameters is ready

view this post on Zulip Pierre-Yves Strub (Jun 02 2020 at 20:06):

Yes, sure, I do remember this. But meanwhile, we could have finset equipped with a porder structure and then move to the general one.


Last updated: Feb 08 2023 at 07:02 UTC