Zulip Chat Archive

Stream: general

Topic: Missing order stuff


Yaël Dillies (Jan 09 2022 at 15:24):

As you may have seen, I'm currently roaming the order library in search of missing instances. Here's my current kill list:

  • Disjoint order on sigma types and its locally finite order instance
  • Locally finite order instance for sum
  • Locally finite order instance on lexicographical prod.
  • Order on tree and its locally finite order instance
  • Prefix order on list and its locally finite order instance

Along with other people, I'm also defining some more order typeclasses and concepts:

If there's any more you want to see, please send it here!


Last updated: Dec 20 2023 at 11:08 UTC