		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)