Top.Util.FiniteSets

A library for finite sets with extensional equality.

Author: Brian Aydemir.

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 :
    ∀ 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.