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
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 map : (int -> int) -> t -> t

map f t

Map the free variables with f

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

up_from delta start t

val up : int -> t -> t

up delta t

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

down_from delta start t

val down : int -> t -> t option

down delta t

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_variable : int -> t -> bool
module Monadic (M : Fmlib.Module_types.MONAD) : sig ... end

Monadic functions

module Inductive : sig ... end

Inductive types