type term = LogtkHOTerm.ttype scope = LogtkSubsts.scopelambda_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).
Abstract successively the given subterms, starting from the right ones. The converse operation is 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.tMatch the first type's arguments with the list.
LogtkType.Error if types are not compatible
val can_apply : LogtkType.t -> LogtkType.t list -> boolCan we apply a term with the given type to terms with the corresponding list of types?
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.
LogtkType.Error if the first term doesn't have a function type or if the types are not compatible