LEXPD : WFFOP

LEXPD is a wff operation.
Converts the wff into the application of a function to the term.
The function is formed by replacing given valid occurrences of a term
with the variable and binding the result.
 
The calling scheme for LEXPD is:

(LEXPD VAR TERM INWFF OCCURS)
"GVAR" "GWFF" "GWFF" "OCC-LIST"


The result is of type GWFF.

The arguments have the following meaning:
VAR : lambda variable
TERM : term to be extracted
INWFF : contracted form
OCCURS : occurrences to be extracted

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage