Ssreflect Users Discussion List

[Chantal KELLER <>]

    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.