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.3.tar.gz

sha256=062f33c55ef39706c4290dff67d5a00bf009051fd757f9352be527f629ae21fc

md5=eb4edc4d6b7e15b83d6397bd34994153

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

Module `Alba_core.Gamma`Source

Sourcetype definition =

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

Sourcetype entry = {

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

}

Sourcetype t

Sourceval empty : t

Sourceval count : t -> int

Sourceval is_valid_index : int -> t -> bool

Sourceval index_of_level : int -> t -> int

Sourceval level_of_index : int -> t -> int

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

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

Sourceval entry : int -> t -> entry

entry level c

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

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

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

Sourceval raw_type_at_level : int -> t -> Term.typ

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

type_at_level level c type of the entry at level.

Sourceval int_type : t -> Term.typ

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

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

Sourceval name_at_level : int -> t -> string

Sourceval name_of_index : int -> t -> string

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

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

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

Sourceval compute : Term.t -> t -> Term.t

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

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

Sourceval add_inductive : Inductive.t -> t -> t