INSTANTIATE-DEFN : WFFOP

INSTANTIATE-DEFN is a wff operation.
Instantiate all occurrences of an abbreviation.
The occurrences will be lambda-contracted, but not lambda-normalized.
 
The calling scheme for INSTANTIATE-DEFN is:

(INSTANTIATE-DEFN GABBR INWFF)
"SYMBOL" "GWFF"


The result is of type GWFF.

The arguments have the following meaning:
GABBR : abbrev
INWFF : inwff

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage