package coq-core

  1. Overview
  2. Docs
package coq-core
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
Constraints.
Sourcetype constraint_type = AcyclicGraph.constraint_type =
  1. | Lt
  2. | Le
  3. | Eq
Sourcetype univ_constraint = Level.t * constraint_type * Level.t
Sourcemodule Constraints : sig ... end
Sourcetype 'a constrained = 'a * Constraints.t

A value with universe Constraints.t.

Sourceval constraints_of : 'a constrained -> Constraints.t

Constrained

Sourcetype 'a constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t

Enforcing Constraints.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 Constraints.t. We linearize the set to a list after typechecking. Beware, representation could change.

Sourcemodule ContextSet : sig ... end
Sourcetype 'a in_universe_context_set = 'a * ContextSet.t

A value in a universe context set.

Substitution
Sourcetype universe_level_subst = Level.t Level.Map.t
Sourceval empty_level_subst : universe_level_subst
Sourceval is_empty_level_subst : universe_level_subst -> bool
Sourceval subst_univs_level_level : universe_level_subst -> Level.t -> Level.t

Substitution of universes.

Sourceval subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t
Sourceval subst_univs_level_constraints : universe_level_subst -> Constraints.t -> Constraints.t
Pretty-printing of universes.
Sourceval pr_constraint_type : constraint_type -> Pp.t
Sourceval pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
Sourceval pr_universe_level_subst : (Level.t -> Pp.t) -> universe_level_subst -> Pp.t
Hash-consing
Sourceval hcons_univ : Universe.t -> Universe.t
Sourceval hcons_constraints : Constraints.t -> Constraints.t
Sourceval hcons_universe_set : Level.Set.t -> Level.Set.t
Sourceval hcons_universe_context_set : ContextSet.t -> ContextSet.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct