Hello! what are the set library recommendations? I'm experienced with `Ensembles`

but i'm looking for something fresh.

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

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

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.

cool, thanks!

Quinn has marked this topic as resolved.

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

ahh, I was hoping `classical_sets`

were in finmap (but probably there are reasons why it isn't...)

Last updated: Feb 06 2023 at 13:03 UTC