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: Mar 28 2024 at 10:01 UTC