Ssreflect Users Discussion List

[Chantal KELLER <>]

A choiceType or a countType instead of an eqType would also be fine (but
not a finType).
Chantal.




Chantal KELLER a écrit :
>     Hello everybody,
> 
>   I am looking for a library of finite sets that would be such that:
>     - the type of the elements of the sets is an eqType
>     - it is computational : for instance, I want [is_empty (remove t
> (remove u (union empty (add t (singleton u)))))] to reduce to true
>     - it has a few usual lemmas (typically, like in the FSetInterface
> library).
> 
>   Many thanks,
>     Chantal.
> 
> 

-- 
Chantal KELLER