package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
Support for universe polymorphism
module Variance : sig ... end
Universe instances
module Instance : sig ... end
val eq_sizes : (int * int) -> (int * int) -> bool

Convenient function to compare the result of Instance.length, UContext.size etc

type 'a quconstraint_function = 'a -> 'a -> Sorts.QUConstraints.t -> Sorts.QUConstraints.t
val enforce_eq_instances : Instance.t quconstraint_function
val enforce_eq_variance_instances : Variance.t array -> Instance.t quconstraint_function
val enforce_leq_variance_instances : Variance.t array -> Instance.t quconstraint_function
type 'a puniverses = 'a * Instance.t
val out_punivs : 'a puniverses -> 'a
val in_punivs : 'a -> 'a puniverses
val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool
type bound_names = Names.Name.t array * Names.Name.t array

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

module UContext : sig ... end

A value in a universe context.

type 'a in_universe_context = 'a * UContext.t

A value in a universe context.

module AbstractContext : sig ... end
type 'a univ_abstracted = {
  1. univ_abstracted_value : 'a;
  2. univ_abstracted_binder : AbstractContext.t;
}

A value with bound universe levels.

val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted
Substitution
val pr_quality_level_subst : (Sorts.QVar.t -> Pp.t) -> Sorts.Quality.t Sorts.QVar.Map.t -> Pp.t
val empty_sort_subst : sort_level_subst
val is_empty_sort_subst : sort_level_subst -> bool
val subst_univs_level_abstract_universe_context : Univ.universe_level_subst -> AbstractContext.t -> AbstractContext.t

There are no constraints on qualities, so this only needs a subst for univs

val subst_sort_level_instance : sort_level_subst -> Instance.t -> Instance.t

Level to universe substitutions.

val subst_sort_level_quality : sort_level_subst -> Sorts.Quality.t -> Sorts.Quality.t
val subst_sort_level_sort : sort_level_subst -> Sorts.t -> Sorts.t
val subst_sort_level_relevance : sort_level_subst -> Sorts.relevance -> Sorts.relevance
val subst_instance_instance : Instance.t -> Instance.t -> Instance.t

Substitution of instances

val subst_instance_universe : Instance.t -> Univ.Universe.t -> Univ.Universe.t
val subst_instance_quality : Instance.t -> Sorts.Quality.t -> Sorts.Quality.t
val subst_instance_sort : Instance.t -> Sorts.t -> Sorts.t
val subst_instance_relevance : Instance.t -> Sorts.relevance -> Sorts.relevance
val subst_instance_sort_level_subst : Instance.t -> sort_level_subst -> sort_level_subst
val make_instance_subst : Instance.t -> sort_level_subst

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

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

TODO: move universe abstraction out of the kernel

val make_abstract_instance : AbstractContext.t -> Instance.t
Pretty-printing of universes.
val pr_universe_context : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> ?variance:Variance.t array -> UContext.t -> Pp.t
val pr_abstract_universe_context : (Sorts.QVar.t -> Pp.t) -> (Univ.Level.t -> Pp.t) -> ?variance:Variance.t array -> AbstractContext.t -> Pp.t
Hash-consing
val hcons_universe_context : UContext.t -> UContext.t
val hcons_abstract_universe_context : AbstractContext.t -> AbstractContext.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