		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)