package alba

  1. Overview
  2. Docs
package alba
Legend:
Library
Module
Module type
Parameter
Class
Class type
include Gamma_algo.GAMMA
type t
val count : t -> int

Number of variables in the context.

val is_valid_index : int -> t -> bool
val name_of_index : int -> t -> string
val push_local : string -> Term.typ -> t -> t

push_local name typ gamma

Add the local variable with name and typ to the context.

Precondition

name <> ""
val type_of_literal : Value.t -> t -> Term.typ
val type_of_variable : int -> t -> Term.typ

type_of_variable idx gamma

Return the type of the variable idx. idx is the De Bruijn index i.e. and index of 0 points to the last variable and an index of count gamma - 1 points to the first variable.

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

definition_term idx gamma

If the variable idx has a definition, then return it. Otherwise return None.

val context : t -> Gamma.t
val expand : Term.t -> t -> Term.t
val is_hole : int -> t -> bool
val value : int -> t -> Term.t option
val fill_hole0 : int -> Term.t -> bool -> t -> t
val fold_entries : (int -> int -> string -> Term.typ -> bool -> Term.t option -> 'a -> 'a) -> t -> 'a -> 'a