		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::add-abbreviation

(primitive) 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).

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-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 instructions.