package alba

  1. Overview
  2. Docs
package alba
Legend:
Library
Module
Module type
Parameter
Class
Class type
val bruijn_convert : int -> int -> int
module Value : sig ... end
module Sort : sig ... end
module Lambda_info : sig ... end
module Pi_info : sig ... end
module Application_info : sig ... end
type t =
  1. | Sort of Sort.t
  2. | Value of Value.t
  3. | Variable of int
  4. | Typed of t * typ
  5. | Appl of t * t * Application_info.t
  6. | Lambda of typ * t * Lambda_info.t
  7. | Pi of typ * typ * Pi_info.t
  8. | Where of string * typ * t * t
    (*

    Where (name, tp, exp, def) is equivalent to the beta redex Appl ( Lambda (tp, exp, "name"), def)

    *)
and typ = t
and formal_argument = string * typ
and inductive
type t_n = t * int
type typ_n = typ * int
val proposition : t
val any : t
val any_uni : int -> t
val variable : int -> t
val application : t -> t -> t
val implicit_application : t -> t -> t
val binary : t -> t -> t -> t
val applications : t -> t list -> t
val lambda0 : string -> bool -> typ -> t -> t
val product0 : string -> bool -> typ -> typ -> typ
val lambda : string -> typ -> t -> t
val product : string -> typ -> typ -> t
val arrow : typ -> typ -> typ
val lambda_untyped : string -> typ -> t -> t
val product_untyped : string -> typ -> typ -> t
val lambda_in : formal_argument list -> t -> t
val product_in : formal_argument list -> t -> t
val expand_where : string -> typ -> t -> t -> t

Rewrite a where block as an application with a lambda term.

val char : int -> t

char code character value.

val string : string -> t

string str string value.

val number_values : string -> t list
val type_of_sort : Sort.t -> typ
val is_sort : typ -> bool
val pi_sort : typ -> typ -> typ
val split_application : t -> t * (t * Application_info.t) list

split_application t

val map : (int -> int) -> t -> t

map f t

Map the free variables with f

val up_from : int -> int -> t -> t

up_from start delta t: increases all free variables >= start in t by delta

requires: 0 <= delta

val up : int -> t -> t

up delta t: increases all free variables in t by delta

requires: 0 <= delta

val up1 : t -> t

up1 t: increases all free variable in t by 1

val down_from : int -> int -> t -> t option

down_from start delta t: decreases all free variables >= start in t by delta if possible. Returns None it there is a free variable in t with index i < delta.

requires: 0 <= delta

val down : int -> t -> t option

down delta t: decreases all free variables in t by delta if possible. Returns None if there is a free variable in t with index i < delta.

requires: 0 <= delta

val substitute0 : (int -> t) -> bool -> t -> t

substitute0 f beta_reduce t

val substitute : (int -> t) -> t -> t

substitute f term substitutes each free variable i in term by the term f i.

val substitute_with_beta : (int -> t) -> t -> t

substitute f term substitutes each free variable i in term by the term f i and do beta reduction in case that f i appears in a function position and is a function abstraction.

val apply : t -> t -> t
val apply_nargs : t -> int -> Application_info.t -> t

apply_nargs f n mode returns

f (Var (n-1)) ... (Var 0)

where all applications are done with mode mode.

val fold_free : (int -> 'a -> 'a) -> t -> 'a -> 'a
val to_index : int -> t -> t
val to_level : int -> t -> t
val has : (int -> bool) -> t -> bool

has p term does the term have a free variable satisfying p?

val forall : (int -> bool) -> t -> bool

forall p term do all free variables in term satisfy p?

val has_variable : int -> t -> bool
module Monadic (M : Fmlib.Module_types.MONAD) : sig ... end

Monadic functions

module Inductive : sig ... end

Inductive types

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