package logtk

  1. Overview
  2. Docs
On This Page
  1. Lambda-Calculus
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.LambdaSource

Lambda-Calculus

Sourcetype term = Term.t
Sourceval whnf : term -> term

Beta-reduce the term into its weak head normal form

Sourceval beta_red_head : term -> term
Sourceval whnf_list : 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 Type.ApplyError

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

Sourceval snf : term -> term

Strong normal form, computing under lambdas and subterms

Sourceval eta_expand : term -> term

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

Sourceval eta_reduce : ?full:bool -> term -> term

Traverse the term, eta-reducing all sub-terms. A term fun x. t x where x ∉ vars(t) becomes t. If full is false, it eta-reduces only at the top level (default: true)

Sourceval is_lambda_pattern : term -> bool
Sourceval is_properly_encoded : term -> bool
Sourcemodule Inner : sig ... end

Low level interface