Module `UVars`Source

Support for universe polymorphism

Sourcemodule Variance : sig ... end

Universe instances

Sourcemodule Instance : sig ... end

Sourceval 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

Sourceval enforce_eq_instances : Instance.t quconstraint_function

Source

val enforce_eq_variance_instances : 
  Variance.t array ->
  Instance.t quconstraint_function

Source

val enforce_leq_variance_instances : 
  Variance.t array ->
  Instance.t quconstraint_function

Sourcetype 'a puniverses = 'a * Instance.t

Sourceval out_punivs : 'a puniverses -> 'a

Sourceval in_punivs : 'a -> 'a puniverses

Source

val eq_puniverses : 
  ('a -> 'a -> bool) ->
  'a puniverses ->
  'a puniverses ->
  bool

Sourcetype 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

Sourcemodule UContext : sig ... end

A value in a universe context.

Sourcetype 'a in_universe_context = 'a * UContext.t

A value in a universe context.

Sourcemodule AbstractContext : sig ... end

Sourcetype 'a univ_abstracted = {

univ_abstracted_value : 'a;
univ_abstracted_binder : AbstractContext.t;

}

A value with bound universe levels.

Source

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

Substitution

Source

val pr_quality_level_subst : 
  (Sorts.QVar.t -> Pp.t) ->
  Sorts.Quality.t Sorts.QVar.Map.t ->
  Pp.t

Source

type sort_level_subst =
  Sorts.Quality.t Sorts.QVar.Map.t * Univ.universe_level_subst

Sourceval empty_sort_subst : sort_level_subst

Sourceval is_empty_sort_subst : sort_level_subst -> bool

Source

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

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

Level to universe substitutions.

Source

val subst_sort_level_quality : 
  sort_level_subst ->
  Sorts.Quality.t ->
  Sorts.Quality.t

Sourceval subst_sort_level_sort : sort_level_subst -> Sorts.t -> Sorts.t

Source

val subst_sort_level_relevance : 
  sort_level_subst ->
  Sorts.relevance ->
  Sorts.relevance

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

Substitution of instances

Sourceval subst_instance_universe : Instance.t -> Univ.Universe.t -> Univ.Universe.t

Sourceval subst_instance_quality : Instance.t -> Sorts.Quality.t -> Sorts.Quality.t

Sourceval subst_instance_sort : Instance.t -> Sorts.t -> Sorts.t

Sourceval subst_instance_relevance : Instance.t -> Sorts.relevance -> Sorts.relevance

Sourceval make_instance_subst : Instance.t -> sort_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

Pretty-printing of universes.

Source

val pr_universe_context : 
  (Sorts.QVar.t -> Pp.t) ->
  (Univ.Level.t -> Pp.t) ->
  ?variance:Variance.t array ->
  UContext.t ->
  Pp.t

Source

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

Sourceval hcons_universe_context : UContext.t -> UContext.t

Sourceval hcons_abstract_universe_context : AbstractContext.t -> AbstractContext.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/UVars/index.html

Module `UVars`Source

Support for universe polymorphism

Universe instances

Substitution

Pretty-printing of universes.

Hash-consing

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/UVars/index.html

Module UVarsSource

Support for universe polymorphism

Universe instances

Substitution

Pretty-printing of universes.

Hash-consing

Module `UVars`Source