		Search-engine friendly clone of the ACL2 documentation.

Translated-terms

Tterm-constant-list

Lift tterm-constant to lists.

Signature
(tterm-constant-list values) → terms
Arguments: values — Guard (value-listp values).
Returns: terms — Type (tterm-listp terms).

Definitions and Theorems

Function: tterm-constant-list

(defun tterm-constant-list (values)
       (declare (xargs :guard (value-listp values)))
       (let ((__function__ 'tterm-constant-list))
            (declare (ignorable __function__))
            (cond ((endp values) nil)
                  (t (cons (tterm-constant (car values))
                           (tterm-constant-list (cdr values)))))))

Theorem: tterm-listp-of-tterm-constant-list

(defthm tterm-listp-of-tterm-constant-list
        (b* ((terms (tterm-constant-list values)))
            (tterm-listp terms))
        :rule-classes :rewrite)

Theorem: tterm-constant-list-of-value-list-fix-values

(defthm tterm-constant-list-of-value-list-fix-values
        (equal (tterm-constant-list (value-list-fix values))
               (tterm-constant-list values)))

Theorem: tterm-constant-list-value-list-equiv-congruence-on-values

(defthm tterm-constant-list-value-list-equiv-congruence-on-values
        (implies (value-list-equiv values values-equiv)
                 (equal (tterm-constant-list values)
                        (tterm-constant-list values-equiv)))
        :rule-classes :congruence)