package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 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 =
  1. | Lt
  2. | Le
  3. | 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_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