Push-untouchable
Add name or list of names to the list of untouchable symbols
Untouchables are functions that cannot be called, as well as state global variables (see programming-with-state) that cannot be
modified or unbound. Macros can also be untouchable in some sense; see defmacro-untouchable.
Examples:
(push-untouchable my-var nil)
(push-untouchable set-mem t)
General Form:
(push-untouchable name{s} fn-p)
where name{s} is a non-nil symbol or a non-nil true list of
symbols, and fn-p is any value (but generally nil or t). If
name{s} is a symbol it is treated as the singleton list containing that
symbol. The effect of this event is to union the given symbols into the list
of ``untouchable variables'' in the current world if fn-p is nil,
else to union the symbols into the list of ``untouchable functions''. This
event is redundant if every symbol listed is already a member of the
appropriate untouchables list (variables or functions).
There is a further restriction on which function names may be made
untouchable: If a function symbol, g, may be introduced into a proof by a
metatheorem (via the metafunction or the hypothesis metafunction) or by a
clause processor and the metatheorem or clause processor has a :well-formedness-guarantee then g may not be made untouchable.
As noted above, macros may not be made directly untouchable; the macro
defmacro-untouchable is provided for that purpose. Thus, it is an
error to evaluate (push-untouchable F t) if F is already a macro
name, and it is also an error to define F as a macro when F has been
made an untouchable function using (push-untouchable F t).
When a symbol is on the untouchables list it is syntactically illegal for
any event to call a function of that name, if fn-p is non-nil, or to
change the value of a state global variable of that name, if fn-p is
nil. Thus, the effect of pushing a function symbol, name, onto
untouchables is to prevent any future event from using that symbol as a
function, or as a state global variable (according to fn-p). This is
generally done to ``fence off'' some primitive function symbol from ``users''
after the developer has used the symbol freely in the development of some
higher level mechanism.
Also see remove-untouchable.
