		Search-engine friendly clone of the ACL2 documentation.

Unquote-term-list

Lift unquote-term to lists.

Signature
(unquote-term-list terms) → values
Arguments: terms — Guard (and (pseudo-term-listp terms) (quote-listp terms)).
Returns: values — Type (true-listp values).

Definitions and Theorems

Function: unquote-term-list

(defun unquote-term-list (terms)
  (declare (xargs :guard (and (pseudo-term-listp terms)
                              (quote-listp terms))))
  (let ((__function__ 'unquote-term-list))
    (declare (ignorable __function__))
    (cond ((endp terms) nil)
          (t (cons (unquote-term (car terms))
                   (unquote-term-list (cdr terms)))))))

Theorem: true-listp-of-unquote-term-list

(defthm true-listp-of-unquote-term-list
  (b* ((values (unquote-term-list terms)))
    (true-listp values))
  :rule-classes :rewrite)