package alba

You can search for identifiers within the package.

in-package search v0.2.0

Alba compiler

Install

sha256=4817038301d3e45bac9edf7e6f2fc8bf0a6d78e76e02ad7ea33ef69bcc17df3b

md5=25234357587126685d64f16236167937

type t

val count : t -> int

val gamma : t -> Gamma.t

val name_map : t -> 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 : Term.t -> t -> Term.t

val push_local : string -> Term.typ -> t -> t

val can_add_global : string -> Term.typ -> t -> bool

val add_axiom : string -> Term.typ -> t -> t

val add_builtin_type : string -> string -> Term.typ -> t -> t

val add_builtin_function : string -> string -> Term.typ -> t -> t

val add_definition : string -> Term.typ -> Term.t -> t -> (t, int) result

val add_inductive : Inductive.t -> t -> t

module Pretty (P : Fmlib.Pretty_printer.SIG) : sig ... end