Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello Felipe,

I know of three implementation of finite sets as quotients on seq. Maybe
one of them fulfills your needs:

1. A simple prototype implementation by Pierre-Yves Strub
https://github.com/strub/ssrmisc

2. A finite set library developed by myself (fset.v) :
https://redmine.ps.uni-saarland.de/projects/completness-and-decidability-for-modal-logics_project/repository/comp-dec-modal-libs

3. The Cyril's Library mentioned below.

Regards
Christian

Am 21.04.2016 um 16:43 schrieb Cyril:
> Dear Felipe,
> uniq asserts that the list contains no duplicates, but in order to
> guarantee the canonicity of the list representing your set, you need a
> little bit more than that, namely the choice of a canonical representative
> for the list of elements, either by sorting them or by using a choice 
> function.
> I have been developing such a library here:
>  https://github.com/Barbichu/finmap
> I'm working on a new revision at the time which will mainly solve some
> inconsistency with the "comprehension" notations.
> Best regards,
>