Library FiniteSets

A library for finite sets with extensional equality.

Author: Brian Aydemir.

Require Import FSets.
Require Import ListFacts.


The following interface wraps the standard library's finite set interface with an additional property: extensional equality.

Module Type S.

  Declare Module E : UsualOrderedType.
  Declare Module F : FSetInterface.S with Module E := E.

  Parameter eq_if_Equal :
    forall s s' : F.t, F.Equal s s' -> s = s'.

End S.


For documentation purposes, we hide the implementation of a functor implementing the above interface. We note only that the implementation here assumes (as an axiom) that proof irrelevance holds.

Module Make (X : UsualOrderedType) <: S with Module E := X.

End Make.