Module `Alba_core.Term`Source

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 =

| Sort of Sort.t
| Value of Value.t
| Variable of int
| Typed of t * typ
| Appl of t * t * Application_info.t
| Lambda of typ * t * Lambda_info.t
| Pi of typ * typ * Pi_info.t
| 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/alba.core/Alba_core/Term/index.html

Module `Alba_core.Term`Source

package alba

Install

Dune Dependency

Authors

Maintainers

Sources

doc/alba.core/Alba_core/Term/index.html

Module Alba_core.TermSource

Module `Alba_core.Term`Source