Library ExtFsetImpl

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].

This page has been generated by coqdoc