		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)