package alba

  1. Overview
  2. Docs
package alba
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Alba_core.TermSource

Sourceval bruijn_convert : int -> int -> int
Sourcemodule Value : sig ... end
Sourcemodule Sort : sig ... end
Sourcemodule Lambda_info : sig ... end
Sourcemodule Pi_info : sig ... end
Sourcemodule Application_info : sig ... end
Sourcetype 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
Sourceand typ = t
Sourceand formal_argument = string * typ
Sourceand inductive
Sourcetype t_n = t * int
Sourcetype typ_n = typ * int
Sourceval proposition : t
Sourceval any : t
Sourceval any_uni : int -> t
Sourceval variable : int -> t
Sourceval application : t -> t -> t
Sourceval implicit_application : t -> t -> t
Sourceval binary : t -> t -> t -> t
Sourceval applications : t -> t list -> t
Sourceval lambda0 : string -> bool -> typ -> t -> t
Sourceval product0 : string -> bool -> typ -> typ -> typ
Sourceval lambda : string -> typ -> t -> t
Sourceval product : string -> typ -> typ -> t
Sourceval arrow : typ -> typ -> typ
Sourceval lambda_untyped : string -> typ -> t -> t
Sourceval product_untyped : string -> typ -> typ -> t
Sourceval lambda_in : formal_argument list -> t -> t
Sourceval product_in : formal_argument list -> t -> t
Sourceval expand_where : string -> typ -> t -> t -> t

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

Sourceval char : int -> t

char code character value.

Sourceval string : string -> t

string str string value.

Sourceval number_values : string -> t list
Sourceval type_of_sort : Sort.t -> typ
Sourceval is_sort : typ -> bool
Sourceval pi_sort : typ -> typ -> typ
Sourceval map : (int -> int) -> t -> t

map f t

Map the free variables with f

Sourceval up_from : int -> int -> t -> t

up_from delta start t

Sourceval up : int -> t -> t

up delta t

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

down_from delta start t

Sourceval down : int -> t -> t option

down delta t

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

substitute0 f beta_reduce t

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

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

Sourceval 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.

Sourceval apply : t -> t -> t
Sourceval 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.

Sourceval fold_free : (int -> 'a -> 'a) -> t -> 'a -> 'a
Sourceval to_index : int -> t -> t
Sourceval to_level : int -> t -> t
Sourceval has_variable : int -> t -> bool
Sourcemodule Monadic (M : Fmlib.Module_types.MONAD) : sig ... end

Monadic functions

Sourcemodule 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