package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Infinite sets over a chosen OrderedType.

All operations over sets are purely applicative (no side-effects).

module type OrderedType = sig ... end

Input signature of the functor Make.

module type S = sig ... end
module Make (Ord : OrderedType) : S with type elt = Ord.t

The Make functor constructs an implementation for any OrderedType.