		Search-engine friendly clone of the ACL2 documentation.

Atc-arrays

Ushort-array-of

Build an array of type unsigned shortfrom a list of its elements.

Signature
(ushort-array-of elements) → array
Arguments: elements — Guard (ushort-listp elements).
Returns: array — Type (ushort-arrayp array).

Definitions and Theorems

Function: ushort-array-of

(defun ushort-array-of (elements)
  (declare (xargs :guard (ushort-listp elements)))
  (declare (xargs :guard (consp elements)))
  (let ((__function__ 'ushort-array-of))
    (declare (ignorable __function__))
    (ushort-array (type-ushort) elements)))

Theorem: ushort-arrayp-of-ushort-array-of

(defthm ushort-arrayp-of-ushort-array-of
  (b* ((array (ushort-array-of elements)))
    (ushort-arrayp array))
  :rule-classes :rewrite)

Theorem: ushort-array-of-of-ushort-array->elements

(defthm ushort-array-of-of-ushort-array->elements
  (equal (ushort-array-of (ushort-array->elements array))
         (ushort-array-fix array)))

Theorem: ushort-array-of-alt-def

(defthm ushort-array-of-alt-def
  (implies (and (ushort-listp elems) (consp elems))
           (equal (ushort-array-of elems)
                  (make-value-array :elemtype (type-ushort)
                                    :elements elems))))

Theorem: ushort-array-of-of-ushort-list-fix-elements

(defthm ushort-array-of-of-ushort-list-fix-elements
  (equal (ushort-array-of (ushort-list-fix elements))
         (ushort-array-of elements)))

Theorem: ushort-array-of-ushort-list-equiv-congruence-on-elements

(defthm ushort-array-of-ushort-list-equiv-congruence-on-elements
  (implies (ushort-list-equiv elements elements-equiv)
           (equal (ushort-array-of elements)
                  (ushort-array-of elements-equiv)))
  :rule-classes :congruence)