Stream: Coq users

Topic: ✔ set library recommendations


view this post on Zulip Quinn (Nov 09 2021 at 20:30):

Hello! what are the set library recommendations? I'm experienced with Ensembles but i'm looking for something fresh.

view this post on Zulip Quinn (Nov 09 2021 at 20:30):

For context, I want to work with slide 5 or this oeis sequence

view this post on Zulip Karl Palmskog (Nov 09 2021 at 20:41):

Recall the tips here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Ensemble.20image/near/260573876

And see the recent discussion here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/aac-tactics.2C.20fset.20automation.2C.20universes

view this post on Zulip Karl Palmskog (Nov 09 2021 at 20:44):

if you want something that extracts well, I recommend the MSet finite set library in Stdlib, in particular, the red-black tree implementation: https://www.cs.princeton.edu/~appel/papers/redblack.pdf -- but the functorial interface can be cumbersome.

view this post on Zulip Quinn (Nov 09 2021 at 22:48):

cool, thanks!

view this post on Zulip Notification Bot (Nov 09 2021 at 23:21):

Quinn has marked this topic as resolved.

view this post on Zulip Reynald Affeldt (Nov 10 2021 at 14:06):

Quinn said:

Hello! what are the set library recommendations? I'm experienced with Ensembles but i'm looking for something fresh.

There is also https://github.com/math-comp/analysis/blob/master/theories/classical_sets.v

view this post on Zulip Karl Palmskog (Nov 10 2021 at 14:46):

ahh, I was hoping classical_sets were in finmap (but probably there are reasons why it isn't...)


Last updated: Oct 03 2023 at 21:01 UTC