		Search-engine friendly clone of the ACL2 documentation.

Values

Value-symbol-list

Lift value-symbol to lists.

Signature
(value-symbol-list symvals) → values
Arguments: symvals — Guard (symbol-value-listp symvals).
Returns: values — Type (value-listp values).

Definitions and Theorems

Function: value-symbol-list

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

Theorem: value-listp-of-value-symbol-list

(defthm value-listp-of-value-symbol-list
        (b* ((values (value-symbol-list symvals)))
            (value-listp values))
        :rule-classes :rewrite)

Theorem: value-symbol-list-of-symbol-value-list-fix-symvals

(defthm value-symbol-list-of-symbol-value-list-fix-symvals
        (equal (value-symbol-list (symbol-value-list-fix symvals))
               (value-symbol-list symvals)))

Theorem: value-symbol-list-symbol-value-list-equiv-congruence-on-symvals

(defthm
     value-symbol-list-symbol-value-list-equiv-congruence-on-symvals
     (implies (symbol-value-list-equiv symvals symvals-equiv)
              (equal (value-symbol-list symvals)
                     (value-symbol-list symvals-equiv)))
     :rule-classes :congruence)