package coq

  1. Overview
  2. No 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.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

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