package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.16.0.tar.gz

sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587

doc/coq-core.clib/Predicate/Make/index.html

Module `Predicate.Make`Source

The Make functor constructs an implementation for any OrderedType.

Parameters

module Ord : OrderedType

Signature

Sourcetype elt = Ord.t

The type of the elements in the set.

Sourcetype t

The type of sets.

Sourceval empty : t

The empty set.

Sourceval full : t

The set of all elements (of type elm).

Sourceval is_empty : t -> bool

Test whether a set is empty or not.

Sourceval is_full : t -> bool

Test whether a set contains the whole type or not.

Sourceval mem : elt -> t -> bool

mem x s tests whether x belongs to the set s.

Sourceval singleton : elt -> t

singleton x returns the one-element set containing only x.

Sourceval add : elt -> t -> t

add x s returns a set containing all elements of s, plus x. If x was already in s, then s is returned unchanged.

Sourceval remove : elt -> t -> t

remove x s returns a set containing all elements of s, except x. If x was not in s, then s is returned unchanged.

Sourceval union : t -> t -> t

Set union.

Sourceval inter : t -> t -> t

Set intersection.

Sourceval diff : t -> t -> t

Set difference.

Sourceval complement : t -> t

Set complement.

Sourceval equal : t -> t -> bool

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

Sourceval subset : t -> t -> bool

subset s1 s2 tests whether the set s1 is a subset of the set s2.

Sourceval elements : t -> bool * elt list

Gives a finite representation of the predicate: if the boolean is false, then the predicate is given in extension. if it is true, then the complement is given

Sourceval is_finite : t -> bool

true if the predicate can be given as a finite set (if elt is a finite type, we can have is_finite x = false yet x is finite, but we don't know how to list its elements)

On This Page

Parameters
Signature