Module Alba_core__.Context

type t
val count : t -> int
val gamma : t -> Alba_core__.Gamma.t
val name_map : t -> Alba_core__.Name_map.t
val index_of_level : int -> t -> int
val level_of_index : int -> t -> int
val empty : t
val find_name : string -> t -> int list
val compute : Alba_core__.Term.t -> t -> Alba_core__.Term.t
val push_local : string -> Alba_core__.Term.typ -> t -> t
val can_add_global : string -> Alba_core__.Term.typ -> t -> bool
val add_axiom : string -> Alba_core__.Term.typ -> t -> t
val add_builtin_type : string -> string -> Alba_core__.Term.typ -> t -> t
val add_builtin_function : string -> string -> Alba_core__.Term.typ -> t -> t
val add_definition : string -> Alba_core__.Term.typ -> Alba_core__.Term.t -> t -> (t, int) Stdlib.result
val add_inductive : Alba_core__.Inductive.t -> t -> t
module Pretty : functor (P : Fmlib.Pretty_printer.SIG) -> sig ... end