		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-reuse

Atj-mark-var-new

Mark a variable as `new'.

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

Definitions and Theorems

Function: atj-mark-var-new

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

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

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