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