		Search-engine friendly clone of the ACL2 documentation.

Atc-arrays

Ushort-array-length

Length of an array of type unsigned short.

Signature
(ushort-array-length array) → length
Arguments: array — Guard (ushort-arrayp array).
Returns: length — Type (posp length).

Definitions and Theorems

Function: ushort-array-length

(defun ushort-array-length (array)
  (declare (xargs :guard (ushort-arrayp array)))
  (let ((__function__ 'ushort-array-length))
    (declare (ignorable __function__))
    (len (ushort-array->elements array))))

Theorem: posp-of-ushort-array-length

(defthm posp-of-ushort-array-length
  (b* ((length (ushort-array-length array)))
    (posp length))
  :rule-classes (:rewrite :type-prescription))

Theorem: natp-of-ushort-array-length

(defthm natp-of-ushort-array-length
  (b* ((length (ushort-array-length array)))
    (natp length))
  :rule-classes :rewrite)

Theorem: ushort-array-length-alt-def

(defthm ushort-array-length-alt-def
  (implies (ushort-arrayp array)
           (equal (ushort-array-length array)
                  (value-array->length array))))

Theorem: ushort-array-length-of-ushort-array-fix-array

(defthm ushort-array-length-of-ushort-array-fix-array
  (equal (ushort-array-length (ushort-array-fix array))
         (ushort-array-length array)))

Theorem: ushort-array-length-ushort-array-equiv-congruence-on-array

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