Univ (p.rocq-runtime.9.2.0.doc.rocq-runtime.kernel.Univ)

Sourcemodule UGlobal : sig ... end

Qualified global universe level

Sourcemodule Level : sig ... end

Universes.

Sourcemodule Universe : sig ... end

univ_level_mem l u Is l is mentioned in u ?

Sourceval univ_level_mem : Level.t -> Universe.t -> bool

univ_level_rem u v min removes u from v, resulting in min if v was exactly u.

Sourceval univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t

Sourcemodule UnivConstraint : sig ... end

Sourcemodule UnivConstraints : sig ... end

type 'a constraint_function =
  'a ->
  'a ->
  UnivConstraints.t ->
  UnivConstraints.t

Enforcing UnivConstraints.t.

Sourceval enforce_eq_level : Level.t constraint_function

Sourceval enforce_leq_level : Level.t constraint_function

Universe contexts (as sets)

A set of universes with universe UnivConstraints.t. We linearize the set to a list after typechecking. Beware, representation could change.

Sourcemodule ContextSet : sig ... end