		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-p-to-stringp-aux

Signature
(4vec-p-to-stringp-aux x.upper x.lower i ac) → *
Arguments: x.upper — Guard (integerp x.upper).; x.lower — Guard (integerp x.lower).; i — Guard (natp i).; ac — Guard (character-listp ac).

Definitions and Theorems

Function: 4vec-p-to-stringp-aux

(defun 4vec-p-to-stringp-aux (x.upper x.lower i ac)
  (declare (xargs :guard (and (integerp x.upper)
                              (integerp x.lower)
                              (natp i)
                              (character-listp ac))))
  (let ((__function__ '4vec-p-to-stringp-aux))
    (declare (ignorable __function__))
    (if (zp i)
        (coerce (reverse ac) 'string)
      (4vec-p-to-stringp-aux
           x.upper x.lower (1- i)
           (cons (4v-to-characterp (logbitp (1- i) x.upper)
                                   (logbitp (1- i) x.lower))
                 ac)))))