Set-default-input-old-to-wrapper-name
Set the default :old-to-wrapper-name input
of APT transformations.
Some APT transformations include an :old-to-wrapper-name input
that specifies the name of the generated theorem
that rewrites (a term involving) a call of the old function
to (a term involving) a call of the wrapper function;
this theorem is generated, and this input is allowed,
only when the wrapper is generated.
When this input is a symbol that is a valid theorem name,
it is used as the theorem name.
When this input is a keyword (which is never a valid theorem name),
the theorem name is the concatenation of
the old function name, the keyword, and the wrapper function name,
e.g. f-to-g if
f is the old function name,
g is the wrapper function name, and
:-to- is the keyword passed as the :old-to-wrapper-name input.
Thus, the keyword specifies a separator
between old and wrapper function names.
The concatenated symbol is in the same package as
the wrapper function name.
This macro sets an entry in the APT defaults table
that provides the default value of the :old-to-wrapper-name input.
It must be a keyword, which is used as a separator as described above.
It would not make sense to have a complete theorem name as default.
The initial value of this default is :-to-.
Macro: set-default-input-old-to-wrapper-name
(defmacro set-default-input-old-to-wrapper-name (kwd)
(declare (xargs :guard (keywordp kwd)))
(cons 'table
(cons *defaults-table-name*
(cons ':old-to-wrapper-name
(cons kwd 'nil)))))