module LogtkLambda:`sig`

..`end`

type`term =`

`LogtkHOTerm.t`

type`scope =`

`LogtkSubsts.scope`

`val beta_reduce : ``?depth:int -> term -> term`

Beta-reduce the term

`val eta_reduce : ``term -> term`

Eta-reduce the term

`val lambda_abstract : ``term -> sub:term -> term`

`lambda_abstract term ~sub`

, applied to a curried term `term`

, and a
subterm `sub`

of `term`

, gives `term'`

such that
`beta_reduce (term' @ sub_t) == term`

holds.
It basically abstracts out `sub`

with a lambda. If `sub`

is not
a subterm of `term`

, then `term' == ^[X]: term`

.
For instance (@ are omitted), `lambda_abstract f(a,g @ b,c) ~sub:g`

will return
the term `^[X]: f(a, X @ b, c)`

.

`val lambda_abstract_list : ``term -> term list -> term`

Abstract successively the given subterms, starting from the
right ones. The converse operation is

`LogtkLambda.lambda_apply_list`

,
that is, `lambda_apply_list (lambda_abstract_list t args) args = t`

should hold.`val match_types : ``?subst:LogtkSubsts.Ty.t ->`

LogtkType.t ->

scope -> LogtkType.t list -> scope -> LogtkSubsts.t

Match the first type's arguments with the list.

**Raises**

`LogtkType.Error`

if types are not compatible`val can_apply : ``LogtkType.t -> LogtkType.t list -> bool`

Can we apply a term with the given type to terms with
the corresponding list of types?

`val lambda_apply_list : ``?depth:int -> term -> term list -> term`

Apply a lambda to a list of arguments.
The type of the lambda must be a generalization of a function
that takes the list's types as arguments.

**Raises**

`LogtkType.Error`

if the first term doesn't have a function type or
if the types are not compatible