Hi. Are `finmap`

s equipped with a porder structure? Otherwise, I'll got for it.

Pierre-Yves Strub said:

Hi. Are

`finmap`

s 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)

finset :)

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

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

and intervals

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

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