Pierre-Yves Strub (Jun 02 2020 at 13:38): Pierre-Yves Strub (Jun 02 2020 at 13:38):Hi. Are finmaps equipped with a porder structure? Otherwise, I'll got for it.
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)
Pierre-Yves Strub (Jun 02 2020 at 15:44):finset :)
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 ...
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
Cyril Cohen (Jun 02 2020 at 16:39):and intervals
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
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: Oct 13 2024 at 01:02 UTC