		Search-engine friendly clone of the ACL2 documentation.

Array2p

Recognize a 2-dimensional array

Example Form:
(array2p 'delta1 a)

General Form:
(array2p name alist)

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

Function: array2p

(defun array2p (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) 2)
          (let ((d1 (car dimensions))
                (d2 (cadr dimensions)))
            (and (integerp d1)
                 (integerp d2)
                 (integerp maximum-length)
                 (< 0 d1)
                 (< 0 d2)
                 (< (* d1 d2) maximum-length)
                 (<= maximum-length
                     (array-maximum-length-bound))
                 (bounded-integer-alistp2 l d1 d2)))))))))