Module Logtk.LambdaSource

Beta-reduce the term into its weak head normal form

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 Type.ApplyError

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

Strong normal form, computing under lambdas and subterms

Traverse the term, eta-expanding all sub-terms. A term t : a -> b becomes fun (x:a). t x

Traverse the term, eta-reducing all sub-terms. A term fun x. t x where x ∉ vars(t) becomes t

Low level interface