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.14.0.tar.gz

sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

doc/coq-core.kernel/Univ/Level/index.html

Module `Univ.Level`Source

Universes.

Sourcemodule UGlobal : sig ... end

Qualified global universe level

Sourcetype t

Type of universe levels. A universe level is essentially a unique name that will be associated to constraints later on. A level can be local to a definition or global.

Sourceval set : t

Sourceval prop : t

Sourceval sprop : t

The set and prop universe levels.

Sourceval is_small : t -> bool

Is the universe set or prop?

Sourceval is_sprop : t -> bool

Sourceval is_prop : t -> bool

Sourceval is_set : t -> bool

Is it specifically Prop or Set

Sourceval compare : t -> t -> int

Comparison function

Sourceval equal : t -> t -> bool

Equality function

Sourceval hash : t -> int

Sourceval make : UGlobal.t -> t

Sourceval pr : t -> Pp.t

Pretty-printing

Sourceval to_string : t -> string

Debug printing

Sourceval var : int -> t

Sourceval var_index : t -> int option

Sourceval name : t -> UGlobal.t option