		Search-engine friendly clone of the ACL2 documentation.

Std/basic

Tuplep

Recognizers for true-lists of some particular length.

(tuplep n x) recognizes n-tuples. For instance:

(tuplep 3 '(1 2 3))     --> t
(tuplep 3 '(1 2))       --> nil (not long enough)
(tuplep 3 '(1 2 3 . 4)) --> nil (not a true-listp)

We generally just leave this enabled.

Definitions and Theorems

Function: tuplep

(defun tuplep (n x)
  (declare (xargs :guard (natp n)))
  (mbe :logic (and (true-listp x) (equal (len x) n))
       :exec (and (true-listp x)
                  (eql (length x) n))))