package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception UniversesDiffer
type t
val empty : t
val make : lbound:UGraph.Bound.t -> UGraph.t -> t
  • deprecated Use from_env
val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> Names.lident list -> t
  • deprecated Use from_env
val from_env : ?binders:Names.lident list -> Environ.env -> t
val of_binders : UnivNames.universe_binders -> t
val of_context_set : Univ.ContextSet.t -> t
val is_empty : t -> bool
val union : t -> t -> t
val context_set : t -> Univ.ContextSet.t
val ugraph : t -> UGraph.t
val initial_graph : t -> UGraph.t
val algebraics : t -> Univ.LSet.t
val constraints : t -> Univ.Constraint.t
val context : t -> Univ.UContext.t
val univ_entry : poly:bool -> t -> Entries.universes_entry
val universe_binders : t -> UnivNames.universe_binders
val add_constraints : t -> Univ.Constraint.t -> t
val add_universe_constraints : t -> UnivProblem.Set.t -> t
val universe_of_name : t -> Names.Id.t -> Univ.Level.t
val restrict_universe_context : lbound:UGraph.Bound.t -> Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t
val restrict : t -> Univ.LSet.t -> t
type rigid =
  1. | UnivRigid
  2. | UnivFlexible of bool
val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
val merge : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> UnivSubst.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
val demote_global_univs : Environ.env -> t -> t
val demote_seff_univs : Univ.LSet.t -> t -> t
val new_univ_variable : ?loc:Loc.t -> rigid -> Names.Id.t option -> t -> t * Univ.Level.t
val add_global_univ : t -> Univ.Level.t -> t
val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
val make_nonalgebraic_variable : t -> Univ.Level.t -> t
val make_flexible_nonalgebraic : t -> t
val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
val normalize_variables : t -> Univ.universe_subst * t
val constrain_variables : Univ.LSet.t -> t -> t
val abstract_undefined_variables : t -> t
val fix_undefined_variables : t -> t
val minimize : t -> t
type (!'a, !'b) gen_universe_decl = {
  1. univdecl_instance : 'a;
  2. univdecl_extensible_instance : bool;
  3. univdecl_constraints : 'b;
  4. univdecl_extensible_constraints : bool;
}
type universe_decl = (Names.lident list, Univ.Constraint.t) gen_universe_decl
val default_univ_decl : universe_decl
val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry
val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
val update_sigma_univs : t -> UGraph.t -> t
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
val id_of_level : t -> Univ.Level.t -> Names.Id.t option
val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct