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

Sourcetype explanation = (constraint_type * Level.t) list

Type explanation is used to decorate error messages to provide useful explanation why a given constraint is rejected. It is composed of a path of universes and relation kinds (r1,u1);..;(rn,un) means .. <(r1) u1 <(r2) ... <(rn) un (where <(ri) is the relation symbol denoted by ri, currently only < and <=). The lowest end of the chain is supposed known (see UniverseInconsistency exn). The upper end may differ from the second univ of UniverseInconsistency because all universes in the path are canonical. Note that each step does not necessarily correspond to an actual constraint, but reflect how the system stores the graph and may result from combination of several Constraints.t...

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

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

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