decidable/finite sets

Stream: new members

[Henning Dieterichs]

I have been using lists so far, but now I need to reason about what happens when merging lists without thinking of duplicates. Since I'm doing program verification, I would like to keep things decidable. I tried using set and item \in set, but I would need decidable item set at many locations for that. Is there some kind of decidable set? In my case, even finite sets would be sufficient.

[Mario Carneiro]

I often use alist and/or finmap for my verified programming needs

[Mario Carneiro]

but I think finset is the most exact match for what you are describing

[Henning Dieterichs]

Thanks, finset seems to be my solution. I had to search a little bit to find the docs though.

[Kevin Buzzard]

Documentation -- we are getting there, but for some of these files which have been around for several years there is certainly still some work to do.

[Kevin Buzzard]

All new files which go into mathlib must have proper documentation, but older files escaped this rule.