package alba

  1. Overview
  2. Docs
Alba compiler

Install 

dune-project
 Dependency

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

Authors

  1. H
    Helmut Brandl <helmut.brandl@gmx.net>

Maintainers

  1. 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.GammaSource

Sourcetype definition =
  1. | Axiom
  2. | Assumption
  3. | Builtin_type of string
  4. | Builtin of string * Term.Value.t
  5. | Definition of Term.t
  6. | Inductive_type of int * int
  7. | Constructor of int * int * int
Sourcetype entry = {
  1. name : string;
  2. typ : Term.typ;
  3. 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