UNTYPED-LAMBDA-NORM : WFFOPUNTYPED-LAMBDA-NORM is a wff operation.
Convert a untyped wff into lambda-normal form. Be aware of unterminated reduction
in untyped lambda calculus.
The calling scheme for UNTYPED-LAMBDA-NORM is:
The result is of type GWFF.
The arguments have the following meaning:
GWFF : gwff
TPS documentation homepage