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
Support for universe polymorphism
Sourcemodule Variance : sig ... end
Universe instances
Sourcemodule Instance : sig ... end
Sourceval enforce_eq_instances : Instance.t constraint_function
Sourceval enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function
Sourceval enforce_leq_variance_instances : Variance.t array -> Instance.t constraint_function
Sourcetype 'a puniverses = 'a * Instance.t
Sourceval out_punivs : 'a puniverses -> 'a
Sourceval in_punivs : 'a -> 'a puniverses
Sourceval eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool

A vector of universe levels with universe Constraints.t, representing local universe variables and associated Constraints.t; the names are user-facing names for printing

Sourcemodule UContext : sig ... end
Sourcemodule AbstractContext : sig ... end
Sourcetype 'a univ_abstracted = {
  1. univ_abstracted_value : 'a;
  2. univ_abstracted_binder : AbstractContext.t;
}

A value with bound universe levels.

Sourceval map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted

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 = 'a * UContext.t

A value in a universe context (resp. context set).

Sourcetype 'a in_universe_context_set = 'a * ContextSet.t
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
Sourceval subst_univs_level_abstract_universe_context : universe_level_subst -> AbstractContext.t -> AbstractContext.t
Sourceval subst_univs_level_instance : universe_level_subst -> Instance.t -> Instance.t

Level to universe substitutions.

Sourceval subst_instance_instance : Instance.t -> Instance.t -> Instance.t

Substitution of instances

Sourceval subst_instance_universe : Instance.t -> Universe.t -> Universe.t
Sourceval make_instance_subst : Instance.t -> universe_level_subst

Creates u(0) ↦ 0; ...; u(n-1) ↦ n - 1 out of u(0); ...; u(n - 1)

Sourceval abstract_universes : UContext.t -> Instance.t * AbstractContext.t

TODO: move universe abstraction out of the kernel

Sourceval make_abstract_instance : AbstractContext.t -> Instance.t
Sourceval compact_univ : Universe.t -> Universe.t * int list

compact_univ u remaps local variables in u such that their indices become consecutive. It returns the new universe and the mapping. Example: compact_univ (Var 0, i); (Prop, 0); (Var 2; j)) = (Var 0,i); (Prop, 0); (Var 1; j), 0; 2

Pretty-printing of universes.
Sourceval pr_constraint_type : constraint_type -> Pp.t
Sourceval pr_constraints : (Level.t -> Pp.t) -> Constraints.t -> Pp.t
Sourceval pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> UContext.t -> Pp.t
Sourceval pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> AbstractContext.t -> 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 : UContext.t -> UContext.t
Sourceval hcons_abstract_universe_context : AbstractContext.t -> AbstractContext.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