add an abbreviation
Major Section: PROOF-CHECKER-COMMANDS
(add-abbreviation v (* x y)) causes future occurrences of
(* x y) to be printed as
(? v), until (unless) a corresponding
remove-abbreviations occurs. In this case we say that
(* x y).
General Form: (add-abbreviation var &optional raw-term)Let
varbe an abbreviation for
raw-termis supplied, else for the current subterm. Note that
varmust 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
expr, an entry
expr is made in an association list, which we will
*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-abbreviationinstruction is successfully invoked. Nevertheless, if one imagines an appropriate redefinition of the ``constant''
*abbreviations-alist*each time an
add-abbreviationis 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
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
abbreviates a term. For example, the second argument of
add-abbreviation may itself use abbreviations that have been defined