		Search-engine friendly clone of the ACL2 documentation.

Revappend-nat-to-bin-chars

Revappend-nat-to-bin-chars-aux

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

Definitions and Theorems

Function: revappend-nat-to-bin-chars-aux

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