package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
module UGlobal : sig ... end

Qualified global universe level

module Level : sig ... end

Universes.

module Universe : sig ... end

univ_level_mem l u Is l is mentioned in u ?

val 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.

val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t
Constraints.
type constraint_type = AcyclicGraph.constraint_type =
  1. | Lt
  2. | Le
  3. | Eq
type univ_constraint = Level.t * constraint_type * Level.t
module Constraints : sig ... end
type 'a constrained = 'a * Constraints.t

A value with universe Constraints.t.

val constraints_of : 'a constrained -> Constraints.t

Constrained

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

Enforcing Constraints.t.

val enforce_eq_level : Level.t constraint_function
val 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.

module ContextSet : sig ... end
type 'a in_universe_context_set = 'a * ContextSet.t

A value in a universe context set.

Substitution
type universe_level_subst = Level.t Level.Map.t
val empty_level_subst : universe_level_subst
val is_empty_level_subst : universe_level_subst -> bool
val subst_univs_level_level : universe_level_subst -> Level.t -> Level.t

Substitution of universes.

val subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t
val subst_univs_level_constraints : universe_level_subst -> Constraints.t -> Constraints.t
Pretty-printing of universes.
val pr_constraint_type : constraint_type -> Pp.t
val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
val pr_universe_level_subst : (Level.t -> Pp.t) -> universe_level_subst -> Pp.t
Hash-consing
val hcons_univ : Universe.t -> Universe.t
val hcons_constraints : Constraints.t -> Constraints.t
val hcons_universe_set : Level.Set.t -> Level.Set.t
val 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