package alba

You can search for identifiers within the package.

in-package search v0.2.0

Alba compiler

Install

Dune Dependency

albatross-lang.sourceforge.net Readme Edit opam file Versions (5)

Authors

H

Helmut Brandl <helmut.brandl@gmx.net>

Maintainers

H

Helmut Brandl <helmut.brandl@gmx.net>

Sources

0.4.4.tar.gz

sha256=4817038301d3e45bac9edf7e6f2fc8bf0a6d78e76e02ad7ea33ef69bcc17df3b

md5=25234357587126685d64f16236167937

doc/alba.core/Alba_core/Gamma/index.html

Module `Alba_core.Gamma`

type definition =

| Axiom
| Assumption
| Builtin_type of string
| Builtin of string * Value.t
| Definition of Term.t
| Inductive_type of int * int
| Constructor of int * int * int

type entry = {

name : string;
typ : Term.typ;
definition : definition;

}

type t

val empty : t

val count : t -> int

val is_valid_index : int -> t -> bool

val index_of_level : int -> t -> int

val level_of_index : int -> t -> int

val level_forall : (int -> bool) -> Term.t -> t -> bool

val level_has : (int -> bool) -> Term.t -> t -> bool

val entry : int -> t -> entry

entry level c

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 raw_type_at_level : int -> t -> Term.typ

val type_at_level : int -> t -> Term.typ

type_at_level level c type of the entry at level.

val int_type : t -> Term.typ

val type_of_literal : Value.t -> t -> Term.typ

val type_of_variable : int -> t -> Term.typ

val name_at_level : int -> t -> string

val name_of_index : int -> t -> string

val variable_at_level : int -> t -> Term.t

val definition_term : int -> t -> Term.t option

val inductive_at_level : int -> t -> Inductive.t option

val compute : Term.t -> t -> Term.t

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

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

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