package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926

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

Module Univ.LevelSource

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
Sourcemodule Set : sig ... end
Sourcemodule Map : sig ... end