		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)