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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct