Library FiniteSets

A library for finite sets with extensional equality.

Author: Brian Aydemir.





Require Import FSets.

Require Import ListFacts.

Interface

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.

Implementation

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.