		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-reuse

Atj-mark-var-old

Mark a variable as `old'.

Signature
(atj-mark-var-old var) → marked-var
Arguments: var — Guard (symbolp var).
Returns: marked-var — Type (symbolp marked-var).

Definitions and Theorems

Function: atj-mark-var-old

(defun atj-mark-var-old (var)
  (declare (xargs :guard (symbolp var)))
  (let ((__function__ 'atj-mark-var-old))
    (declare (ignorable __function__))
    (packn-pos (list "[O]" var) var)))

Theorem: symbolp-of-atj-mark-var-old

(defthm symbolp-of-atj-mark-var-old
  (b* ((marked-var (atj-mark-var-old var)))
    (symbolp marked-var))
  :rule-classes :rewrite)