		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
                        *maximum-positive-32-bit-integer*)
                    (bounded-integer-alistp2 l d1 d2)))))))))