unsigned-byte-listp-def

other

(in-package "ACL2")

unsigned-byte-listpfunction

(defund unsigned-byte-listp
  (n x)
  (declare (xargs :guard t))
  (if (atom x)
    (null x)
    (and (unsigned-byte-p n (car x))
      (unsigned-byte-listp n (cdr x)))))