LEXP : EDOPLEXP is an editor command.
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 command format for LEXP is:
<Ed>LEXP VAR TERM <<INWFF>> OCCURS
"GVAR" "GWFF" <<GWFF>> "OCC-LIST"
The result replaces the current wff.
TPS documentation homepage