← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to lib/predicate.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
lib/predicate.mli
 
1
 
 
2
(*i $Id: predicate.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
 
3
 
 
4
(* Module [Pred]: sets over infinite ordered types with complement. *)
 
5
 
 
6
(* This module implements the set data structure, given a total ordering
 
7
   function over the set elements. All operations over sets
 
8
   are purely applicative (no side-effects).
 
9
   The implementation uses the Set library. *)
 
10
 
 
11
module type OrderedType =
 
12
  sig
 
13
    type t
 
14
    val compare: t -> t -> int
 
15
  end
 
16
          (* The input signature of the functor [Pred.Make].
 
17
             [t] is the type of the set elements.
 
18
             [compare] is a total ordering function over the set elements.
 
19
             This is a two-argument function [f] such that
 
20
             [f e1 e2] is zero if the elements [e1] and [e2] are equal,
 
21
             [f e1 e2] is strictly negative if [e1] is smaller than [e2],
 
22
             and [f e1 e2] is strictly positive if [e1] is greater than [e2].
 
23
             Example: a suitable ordering function is
 
24
             the generic structural comparison function [compare]. *)
 
25
 
 
26
module type S =
 
27
  sig
 
28
    type elt
 
29
          (* The type of the set elements. *)
 
30
    type t
 
31
          (* The type of sets. *)
 
32
    val empty: t
 
33
          (* The empty set. *)
 
34
    val full: t
 
35
          (* The whole type. *)
 
36
    val is_empty: t -> bool
 
37
        (* Test whether a set is empty or not. *)
 
38
    val is_full: t -> bool
 
39
        (* Test whether a set contains the whole type or not. *)
 
40
    val mem: elt -> t -> bool
 
41
        (* [mem x s] tests whether [x] belongs to the set [s]. *)
 
42
    val singleton: elt -> t
 
43
        (* [singleton x] returns the one-element set containing only [x]. *)
 
44
    val add: elt -> t -> t
 
45
        (* [add x s] returns a set containing all elements of [s],
 
46
           plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
 
47
    val remove: elt -> t -> t
 
48
        (* [remove x s] returns a set containing all elements of [s],
 
49
           except [x]. If [x] was not in [s], [s] is returned unchanged. *)
 
50
    val union: t -> t -> t
 
51
    val inter: t -> t -> t
 
52
    val diff: t -> t -> t
 
53
    val complement: t -> t
 
54
        (* Union, intersection, difference and set complement. *)
 
55
    val equal: t -> t -> bool
 
56
        (* [equal s1 s2] tests whether the sets [s1] and [s2] are
 
57
           equal, that is, contain equal elements. *)
 
58
    val subset: t -> t -> bool
 
59
        (* [subset s1 s2] tests whether the set [s1] is a subset of
 
60
           the set [s2]. *)
 
61
    val elements: t -> bool * elt list
 
62
        (* Gives a finite representation of the predicate: if the
 
63
           boolean is false, then the predicate is given in extension.
 
64
           if it is true, then the complement is given *)
 
65
  end
 
66
 
 
67
module Make(Ord: OrderedType): (S with type elt = Ord.t)
 
68
        (* Functor building an implementation of the set structure
 
69
           given a totally ordered type. *)