		Search-engine friendly clone of the ACL2 documentation.

Atc-arrays

Ushort-array

Fixtype of (ATC's model of) arrays of type unsigned short.

This is a product type introduced by fty::defprod.

Fields

elemtype — type
elements — ushort-list

Additional Requirements

The following invariant is enforced on the fields:

(and (type-case elemtype :ushort) (consp elements))

Theorem: ushort-arrayp-alt-def

(defthm ushort-arrayp-alt-def
  (equal (ushort-arrayp x)
         (and (valuep x)
              (value-case x :array)
              (equal (value-array->elemtype x)
                     (type-ushort))
              (ushort-listp (value-array->elements x)))))

Theorem: ushort-array->elements-alt-def

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

Subtopics

Ushort-array-fix: Fixing function for ushort-array structures.
Ushort-array-equiv: Basic equivalence relation for ushort-array structures.
Make-ushort-array: Basic constructor macro for ushort-array structures.
Ushort-arrayp: Recognizer for ushort-array structures.
Ushort-array->elemtype: Get the elemtype field from a ushort-array.
Ushort-array->elements: Get the elements field from a ushort-array.
Change-ushort-array: Modifying constructor for ushort-array structures.