Library FiniteSets
A library for finite sets with extensional equality.
Author: Brian Aydemir.
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.