		Search-engine friendly clone of the ACL2 documentation.

Nat-to-bin-chars

Nat-to-bin-chars-aux

Signature
(nat-to-bin-chars-aux n acc) → *
Arguments: n — Guard (natp n).

Definitions and Theorems

Function: nat-to-bin-chars-aux

(defun nat-to-bin-chars-aux (n acc)
 (declare (xargs :guard (natp n)))
 (let ((acl2::__function__ 'nat-to-bin-chars-aux))
  (declare (ignorable acl2::__function__))
  (mbe
    :logic
    (revappend (basic-nat-to-bin-chars n)
               acc)
    :exec
    (if (zp n)
        acc
      (nat-to-bin-chars-aux (the unsigned-byte
                                 (ash (the unsigned-byte n) -1))
                            (cons (if (eql (the bit (logand n 1)) 1)
                                      #\1
                                    #\0)
                                  acc))))))