		Search-engine friendly clone of the ACL2 documentation.

Values

Value-list-of

Make a meta-level list value from a list of meta-level values.

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

Definitions and Theorems

Function: value-list-of

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

Theorem: valuep-of-value-list-of

(defthm valuep-of-value-list-of
  (b* ((value (value-list-of values)))
    (valuep value))
  :rule-classes :rewrite)

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

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

Theorem: value-list-of-value-list-equiv-congruence-on-values

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