		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-reuse

Atj-mark-vars-new

Lift atj-mark-var-new to lists.

Signature
(atj-mark-vars-new vars) → marked-vars
Arguments: vars — Guard (symbol-listp vars).
Returns: marked-vars — Type (symbol-listp marked-vars).

Definitions and Theorems

Function: atj-mark-vars-new

(defun atj-mark-vars-new (vars)
  (declare (xargs :guard (symbol-listp vars)))
  (let ((__function__ 'atj-mark-vars-new))
    (declare (ignorable __function__))
    (cond ((endp vars) nil)
          (t (cons (atj-mark-var-new (car vars))
                   (atj-mark-vars-new (cdr vars)))))))

Theorem: symbol-listp-of-atj-mark-vars-new

(defthm symbol-listp-of-atj-mark-vars-new
  (b* ((marked-vars (atj-mark-vars-new vars)))
    (symbol-listp marked-vars))
  :rule-classes :rewrite)

Theorem: len-of-atj-mark-vars-new

(defthm len-of-atj-mark-vars-new
  (b* ((?marked-vars (atj-mark-vars-new vars)))
    (equal (len marked-vars) (len vars))))