Module `Univ`Source

Sourcemodule Level : sig ... end

Universes.

Sourcemodule LSet : sig ... end

Sourcemodule Universe : sig ... end

Alias name.

Sourceval pr_uni : Universe.t -> Pp.t

Sourceval type0m_univ : Universe.t

The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0

Sourceval type0_univ : Universe.t

Sourceval type1_univ : Universe.t

Sourceval is_type0_univ : Universe.t -> bool

Sourceval is_type0m_univ : Universe.t -> bool

Sourceval is_univ_variable : Universe.t -> bool

Sourceval is_small_univ : Universe.t -> bool

Sourceval sup : Universe.t -> Universe.t -> Universe.t

Sourceval super : Universe.t -> Universe.t

Sourceval universe_level : Universe.t -> Level.t option

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

Sourcemodule Constraint : sig ... end

Sourceval empty_constraint : Constraints.t

Sourceval union_constraint : Constraints.t -> Constraints.t -> Constraints.t

Sourceval eq_constraint : Constraints.t -> Constraints.t -> bool

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 : Universe.t constraint_function

Sourceval enforce_leq : Universe.t constraint_function

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...

Source

type univ_inconsistency =
  constraint_type * Universe.t * Universe.t * explanation Lazy.t option

Sourceexception UniverseInconsistency of univ_inconsistency

Support for universe polymorphism

Sourcemodule LMap : sig ... end

Sourcetype 'a universe_map = 'a Level.Map.t

Substitution

Sourcetype universe_subst_fn = Level.t -> Universe.t

Sourcetype universe_level_subst_fn = Level.t -> Level.t

Sourcetype universe_subst = Universe.t universe_map

A full substitution, might involve algebraic universes

Sourcetype universe_level_subst = Level.t universe_map

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

Sourcemodule AUContext : 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

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 make_subst : universe_subst -> universe_subst_fn

Sourceval subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t

Only user in the kernel is template polymorphism. Ideally we get rid of this code if it goes away.

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 make_inverse_instance_subst : Instance.t -> universe_level_subst

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

Source

val explain_universe_inconsistency : 
  (Level.t -> Pp.t) ->
  univ_inconsistency ->
  Pp.t

Sourceval pr_universe_level_subst : universe_level_subst -> Pp.t

Sourceval pr_universe_subst : universe_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

Substitution

Universe instances

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

Substitution

Universe instances

Pretty-printing of universes.

Hash-consing

Module `Univ`Source