Finset for computation

Stream: Is there code for X?

[yokatta]

Is there something like Finset that is suited to both proofs and computation (in particular has a defined ordering)? Was looking at RBSet, but I'm unsure if it has the same equality behavior (if you converted two permuted lists into an RBSet, would they always be equal?)

[Mario Carneiro]

you could use sorted lists, or RBSet quotient by toList

[Mario Carneiro]

I've never really seen a good reason to explicitly construct the quotient though, when reasoning about RBSet. Just state theorems with an appropriate relation instead of equality