Require Import Bool.
Require Import List.
Require Import OrderedType.
Require Import SetoidList.
Require Import Axioms.
Require Export ExtFset.
Set Implicit Arguments.
Unset Strict Implicit.
| The main purpose of this file is to provide an implementation of the following module signature. We use modules here to purposefully keep the implementation opaque. |
Module Type ExtFsetSig.
Parameter mkOrderedListExtFset
: forall (elt : Set) (lt : elt -> elt -> Prop),
(forall x y z : elt, lt x y -> lt y z -> lt x z) ->
(forall x y : elt, lt x y -> x <> y) ->
(forall x y : elt, Compare lt (eq (A:=elt)) x y) -> ExtFset elt.
End ExtFsetSig.
Module ExtFsetImplementation : ExtFsetSig.
| Hide the implementation for documentation purposes. Note that we need proof irrelevance here. |
End ExtFsetImplementation.
Export ExtFsetImplementation.
Implicit Arguments mkOrderedListExtFset [elt].