SUBSTITUTE-BDVAR-SCOPE : WFFOPSUBSTITUTE-BDVAR-SCOPE is a wff operation.
Creates instantiation from binder definition, etc.
The calling scheme for SUBSTITUTE-BDVAR-SCOPE is:
(SUBSTITUTE-BDVAR-SCOPE DEF-VAR NEWVAR SCOPE-VAR SCOPE INWFF)
"GVAR" "GVAR" "GVAR" "GWFF" "GWFF"
The result is of type GWFF.
The arguments have the following meaning:
DEF-VAR : Old bound variable
NEWVAR : New bound variable
SCOPE-VAR : Variable for which scope is substituted
SCOPE : Scope of instantiated binder
INWFF : NIL
TPS documentation homepage