		Search-engine friendly clone of the ACL2 documentation.

Tuple-operations

Op-tuple-make

Leo tuple construction operation.

Signature
(op-tuple-make vals) → result
Arguments: vals — Guard (value-listp vals).
Returns: result — Type (valuep result).

A tuple in Leo is constructed from two or more values. However, here we also allow tuples of zero or one value. Tuples of zero values are constructed from the unit expression. There is no syntax in Leo to construct tuples of 1 value. The values may have any types. This operation never fails.

Definitions and Theorems

Function: op-tuple-make

(defun op-tuple-make (vals)
  (declare (xargs :guard (value-listp vals)))
  (let ((__function__ 'op-tuple-make))
    (declare (ignorable __function__))
    (value-tuple vals)))

Theorem: valuep-of-op-tuple-make

(defthm valuep-of-op-tuple-make
  (b* ((result (op-tuple-make vals)))
    (valuep result))
  :rule-classes :rewrite)

Theorem: op-tuple-make-of-value-list-fix-vals

(defthm op-tuple-make-of-value-list-fix-vals
  (equal (op-tuple-make (value-list-fix vals))
         (op-tuple-make vals)))

Theorem: op-tuple-make-value-list-equiv-congruence-on-vals

(defthm op-tuple-make-value-list-equiv-congruence-on-vals
  (implies (value-list-equiv vals vals-equiv)
           (equal (op-tuple-make vals)
                  (op-tuple-make vals-equiv)))
  :rule-classes :congruence)