		Search-engine friendly clone of the ACL2 documentation.

Array1p

Recognize a 1-dimensional array

Example Form:
(array1p 'delta1 a)

General Form:
(array1p name alist)

where name and alist are arbitrary objects. This function returns t if alist is a 1-dimensional ACL2 array. Otherwise it returns nil. The function operates in constant time if alist is the semantic value of name. See arrays.

Function: array1p

(defun array1p (name l)
 (declare (xargs :guard t))
 (and
  (symbolp name)
  (alistp l)
  (let ((header-keyword-list (cdr (assoc-eq :header l))))
   (and
    (keyword-value-listp header-keyword-list)
    (let
     ((dimensions
           (cadr (assoc-keyword :dimensions header-keyword-list)))
      (maximum-length
        (cadr (assoc-keyword :maximum-length header-keyword-list))))
     (and (true-listp dimensions)
          (equal (length dimensions) 1)
          (integerp (car dimensions))
          (integerp maximum-length)
          (< 0 (car dimensions))
          (< (car dimensions) maximum-length)
          (<= maximum-length
              (array-maximum-length-bound))
          (bounded-integer-alistp l (car dimensions))))))))