Library Coq.FSets.FSetList



Finite sets library


This file proposes an implementation of the non-dependant interface FSetInterface.S using strictly ordered list.

Require Export FSetInterface.

This is just a compatibility layer, the real implementation is now in MSetList

Require FSetCompat MSetList Orders OrdersAlt.

Module Make (X: OrderedType) <: S with Module E := X.
 Module X' := OrdersAlt.Update_OT X.
 Module MSet := MSetList.Make X'.
 Include FSetCompat.Backport_Sets X MSet.
End Make.