package rocq-runtime

  1. Overview
  2. Docs
On This Page
  1. UnivConstraints.
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module UnivSource

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
UnivConstraints.
Sourcemodule UnivConstraint : sig ... end
Sourcemodule UnivConstraints : sig ... end
Sourcetype '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