package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.kernel/Names/KNpred/index.html

Module `Names.KNpred`

type elt = KerName.t

The type of the elements in the set.

type t

The type of sets.

val empty : t

The empty set.

val full : t

The set of all elements (of type elm).

val is_empty : t -> bool

Test whether a set is empty or not.

val is_full : t -> bool

Test whether a set contains the whole type or not.

val mem : elt -> t -> bool

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

val singleton : elt -> t

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

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

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

val union : t -> t -> t

Set union.

val inter : t -> t -> t

Set intersection.

val diff : t -> t -> t

Set difference.

val complement : t -> t

Set complement.

val equal : t -> t -> bool

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

val subset : t -> t -> bool

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

val 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

val 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)