coq 8.9.1 · OCaml Package

coq

module Level : sig ... end

type universe_level = Level.t

deprecated Use Level.t

module LSet : sig ... end

type universe_set = LSet.t

deprecated Use LSet.t

module Universe : sig ... end

type universe = Universe.t

deprecated Use Universe.t

val pr_uni : Universe.t -> Pp.t

val type0m_univ : Universe.t

val type0_univ : Universe.t

val type1_univ : Universe.t

val is_type0_univ : Universe.t -> bool

val is_type0m_univ : Universe.t -> bool

val is_univ_variable : Universe.t -> bool

val is_small_univ : Universe.t -> bool

val sup : Universe.t -> Universe.t -> Universe.t

val super : Universe.t -> Universe.t

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

val univ_level_mem : Level.t -> Universe.t -> bool

val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t

type constraint_type =

| Lt
| Le
| Eq

type univ_constraint = Level.t * constraint_type * Level.t

module Constraint : sig ... end

type constraints = Constraint.t

deprecated Use Constraint.t

val empty_constraint : Constraint.t

val union_constraint : Constraint.t -> Constraint.t -> Constraint.t

val eq_constraint : Constraint.t -> Constraint.t -> bool

type !'a constrained = 'a * Constraint.t

val constraints_of : 'a constrained -> Constraint.t

type !'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t

val enforce_eq : Universe.t constraint_function

val enforce_leq : Universe.t constraint_function

val enforce_eq_level : Level.t constraint_function

val enforce_leq_level : Level.t constraint_function

type explanation = (constraint_type * Universe.t) list

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

exception UniverseInconsistency of univ_inconsistency

module LMap : sig ... end

type 'a universe_map = 'a LMap.t

type universe_subst_fn = Level.t -> Universe.t

type universe_level_subst_fn = Level.t -> Level.t

type universe_subst = Universe.t universe_map

type universe_level_subst = Level.t universe_map

module Variance : sig ... end

module Instance : sig ... end

type universe_instance = Instance.t

deprecated Use Instance.t

val enforce_eq_instances : Instance.t constraint_function

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

val enforce_leq_variance_instances : 
  Variance.t array ->
  Instance.t constraint_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

module UContext : sig ... end

type universe_context = UContext.t

deprecated Use UContext.t

module AUContext : sig ... end

type abstract_universe_context = AUContext.t

deprecated Use AUContext.t

module CumulativityInfo : sig ... end

type cumulativity_info = CumulativityInfo.t

deprecated Use CumulativityInfo.t

module ACumulativityInfo : sig ... end

type abstract_cumulativity_info = ACumulativityInfo.t

deprecated Use ACumulativityInfo.t

module ContextSet : sig ... end

type universe_context_set = ContextSet.t

deprecated Use ContextSet.t

type !'a in_universe_context = 'a * UContext.t

type !'a in_universe_context_set = 'a * ContextSet.t

val empty_level_subst : universe_level_subst

val is_empty_level_subst : universe_level_subst -> bool

val subst_univs_level_level : universe_level_subst -> Level.t -> Level.t

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

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

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

val subst_univs_level_instance : 
  universe_level_subst ->
  Instance.t ->
  Instance.t

val empty_subst : universe_subst

val is_empty_subst : universe_subst -> bool

val make_subst : universe_subst -> universe_subst_fn

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

val subst_instance_instance : Instance.t -> Instance.t -> Instance.t

val subst_instance_universe : Instance.t -> Universe.t -> Universe.t

val make_instance_subst : Instance.t -> universe_level_subst

val make_inverse_instance_subst : Instance.t -> universe_level_subst

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

val abstract_cumulativity_info : 
  CumulativityInfo.t ->
  Instance.t * ACumulativityInfo.t

val make_abstract_instance : AUContext.t -> Instance.t

val compact_univ : Universe.t -> Universe.t * int list

val pr_constraint_type : constraint_type -> Pp.t

val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t

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

val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t

val pr_abstract_universe_context : 
  (Level.t -> Pp.t) ->
  ?variance:Variance.t array ->
  AUContext.t ->
  Pp.t

val pr_abstract_cumulativity_info : 
  (Level.t -> Pp.t) ->
  ACumulativityInfo.t ->
  Pp.t

val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t

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

val pr_universe_level_subst : universe_level_subst -> Pp.t

val pr_universe_subst : universe_subst -> Pp.t

val hcons_univ : Universe.t -> Universe.t

val hcons_constraints : Constraint.t -> Constraint.t

val hcons_universe_set : LSet.t -> LSet.t

val hcons_universe_context : UContext.t -> UContext.t

val hcons_abstract_universe_context : AUContext.t -> AUContext.t

val hcons_universe_context_set : ContextSet.t -> ContextSet.t

val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t

val hcons_abstract_cumulativity_info : 
  ACumulativityInfo.t ->
  ACumulativityInfo.t

val compare_levels : Level.t -> Level.t -> int

deprecated Use Level.compare

val eq_levels : Level.t -> Level.t -> bool

deprecated Use Level.equal

val equal_universes : Universe.t -> Universe.t -> bool

deprecated Use Universe.equal

val universes_of_constraints : Constraint.t -> LSet.t

deprecated Use Constraint.universes_of

package coq