Module `Univ`Source

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 =

| Lt
| Le
| 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

Source

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

Source

val 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

Source

val 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 = {

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

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

Source

val extend_in_context_set : 
  'a in_universe_context_set ->
  ContextSet.t ->
  'a in_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.

Source

val subst_univs_level_universe : 
  universe_level_subst ->
  Universe.t ->
  Universe.t

Source

val subst_univs_level_constraints : 
  universe_level_subst ->
  Constraints.t ->
  Constraints.t

Source

val subst_univs_level_abstract_universe_context : 
  universe_level_subst ->
  AbstractContext.t ->
  AbstractContext.t

Source

val 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

Source

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

Source

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

Sourcetype explanation = Level.t * (constraint_type * Level.t) list

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Univ`Source

Constraints.

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/Univ/index.html

Module UnivSource

Constraints.

Support for universe polymorphism

Universe instances

Substitution

Pretty-printing of universes.

Hash-consing

Module `Univ`Source