Library Coq.FSets.FSetWeakList


Finite sets library

This file proposes an implementation of the non-dependant interface FSetInterface.WS using lists without redundancy.

Require Import FSetInterface.
Set Implicit Arguments.

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

Require Equalities FSetCompat MSetWeakList.

Module Make (X: DecidableType) <: WS with Module E := X.
 Module E := X.
 Module X´ := Equalities.Update_DT X.
 Module MSet := MSetWeakList.Make X´.
 Include FSetCompat.Backport_WSets X MSet.
End Make.