		Search-engine friendly clone of the ACL2 documentation.

Tuple-operations

Op-tuple-read

Leo tuple reading operation.

Signature
(op-tuple-read tupval index) → result
Arguments: tupval — Guard (valuep tupval).; index — Guard (natp index).
Returns: result — Type (value-resultp result).

This takes a value and a natural number index; the latter must be a numeral in the syntax. The value must be a tuple, otherwise it is an error. Furthermore, the index must be below the tuple length; tuples are zero-indexed.

Definitions and Theorems

Function: op-tuple-read

(defun op-tuple-read (tupval index)
  (declare (xargs :guard (and (valuep tupval) (natp index))))
  (let ((__function__ 'op-tuple-read))
    (declare (ignorable __function__))
    (if (and (value-case tupval :tuple)
             (< (nfix index)
                (len (value-tuple->components tupval))))
        (nth (nfix index)
             (value-tuple->components tupval))
      (reserrf (list :op-tuple-read (value-fix tupval)
                     (nfix index))))))

Theorem: value-resultp-of-op-tuple-read

(defthm value-resultp-of-op-tuple-read
  (b* ((result (op-tuple-read tupval index)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-tuple-read-of-value-fix-tupval

(defthm op-tuple-read-of-value-fix-tupval
  (equal (op-tuple-read (value-fix tupval) index)
         (op-tuple-read tupval index)))

Theorem: op-tuple-read-value-equiv-congruence-on-tupval

(defthm op-tuple-read-value-equiv-congruence-on-tupval
  (implies (value-equiv tupval tupval-equiv)
           (equal (op-tuple-read tupval index)
                  (op-tuple-read tupval-equiv index)))
  :rule-classes :congruence)

Theorem: op-tuple-read-of-nfix-index

(defthm op-tuple-read-of-nfix-index
  (equal (op-tuple-read tupval (nfix index))
         (op-tuple-read tupval index)))

Theorem: op-tuple-read-nat-equiv-congruence-on-index

(defthm op-tuple-read-nat-equiv-congruence-on-index
  (implies (acl2::nat-equiv index index-equiv)
           (equal (op-tuple-read tupval index)
                  (op-tuple-read tupval index-equiv)))
  :rule-classes :congruence)