		Search-engine friendly clone of the ACL2 documentation.

Utilities

All-have-len

(all-have-len x n) determines if every element of x has length n.

Signature
(all-have-len x n) → *

Definitions and Theorems

Function: all-have-len

(defun all-have-len (x n)
  (declare (xargs :guard t))
  (let ((__function__ 'all-have-len))
    (declare (ignorable __function__))
    (if (consp x)
        (and (eql (len (car x)) n)
             (all-have-len (cdr x) n))
      t)))

Theorem: all-have-len-when-not-consp

(defthm all-have-len-when-not-consp
  (implies (not (consp x))
           (all-have-len x n)))

Theorem: all-have-len-of-cons

(defthm all-have-len-of-cons
  (equal (all-have-len (cons a x) n)
         (and (equal (len a) n)
              (all-have-len x n))))

Theorem: all-have-len-of-strip-cdrs

(defthm all-have-len-of-strip-cdrs
  (implies (and (not (zp n)) (all-have-len x n))
           (all-have-len (strip-cdrs x) (1- n))))

Theorem: alistp-when-all-have-len

(defthm alistp-when-all-have-len
  (implies (and (not (zp n)) (all-have-len x n))
           (equal (alistp x) (true-listp x))))