		Search-engine friendly clone of the ACL2 documentation.

Array-operations

Value-array->length

Length of an array.

Signature
(value-array->length array) → length
Arguments: array — Guard (valuep array).
Returns: length — Type (posp length).

Definitions and Theorems

Function: value-array->length

(defun value-array->length (array)
  (declare (xargs :guard (valuep array)))
  (declare (xargs :guard (value-case array :array)))
  (let ((__function__ 'value-array->length))
    (declare (ignorable __function__))
    (len (value-array->elements array))))

Theorem: posp-of-value-array->length

(defthm posp-of-value-array->length
  (b* ((length (value-array->length array)))
    (posp length))
  :rule-classes :rewrite)

Theorem: value-array->length-of-value-fix-array

(defthm value-array->length-of-value-fix-array
  (equal (value-array->length (value-fix array))
         (value-array->length array)))

Theorem: value-array->length-value-equiv-congruence-on-array

(defthm value-array->length-value-equiv-congruence-on-array
  (implies (value-equiv array array-equiv)
           (equal (value-array->length array)
                  (value-array->length array-equiv)))
  :rule-classes :congruence)