add an abbreviation
Major Section: PROOF-CHECKER-COMMANDS
Example: (add-abbreviation v (* x y)) causes future occurrences of
(* x y) to be printed as (? v), until (unless) a corresponding
invocation of remove-abbreviations occurs. In this case we say that
v ``abbreviates'' (* x y).
General Form: (add-abbreviation var &optional raw-term)Let
var be an abbreviation for raw-term, if raw-term is supplied,
else for the current subterm. Note that var must be a variable that
does not already abbreviate some term.A way to think of abbreviations is as follows. Imagine that
whenever an abbreviation is added, say v abbreviates expr, an entry
associating v to expr is made in an association list, which we will
call ``*abbreviations-alist*''. Then simply imagine that ? is a
function defined by something like:
(defun ? (v)
(let ((pair (assoc v *abbreviations-alist*)))
(if pair (cdr pair)
(error ...))))
Of course the implementation isn't exactly like that, since the
``constant'' *abbreviations-alist* actually changes each time an
add-abbreviation instruction is successfully invoked. Nevertheless,
if one imagines an appropriate redefinition of the ``constant''
*abbreviations-alist* each time an add-abbreviation is invoked, then
one will have a clear model of the meaning of such an instruction.The effect of abbreviations on output is that before printing a
term, each subterm that is abbreviated by a variable v is first
replaced by (? v).
The effect of abbreviations on input is that every built-in
proof-checker command accepts abbreviations wherever a term is
expected as an argument, i.e., accepts the syntax (? v) whenever v
abbreviates a term. For example, the second argument of
add-abbreviation may itself use abbreviations that have been defined
by previous add-abbreviation instructions.
See also remove-abbreviations and show-abbreviations.
