add an abbreviation
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).
(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)
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 (?
The effect of abbreviations on input is that every built-in proof-builder
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
See also ACL2-pc::remove-abbreviations and see ACL2-pc::show-abbreviations.