package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Level : sig ... end
module LSet : sig ... end
module Universe : sig ... end
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 = AcyclicGraph.constraint_type =
  1. | Lt
  2. | Le
  3. | Eq
type univ_constraint = Level.t * constraint_type * Level.t
module Constraint : sig ... end
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 * Level.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
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
module AUContext : sig ... end
type !'a univ_abstracted = {
  1. univ_abstracted_value : 'a;
  2. univ_abstracted_binder : AUContext.t;
}
val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted
module ContextSet : sig ... end
type !'a in_universe_context = 'a * UContext.t
type !'a in_universe_context_set = 'a * ContextSet.t
val extend_in_context_set : 'a in_universe_context_set -> ContextSet.t -> 'a in_universe_context_set
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 : Names.Name.t array -> UContext.t -> Instance.t * AUContext.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_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array -> AUContext.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