		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))))