(nat-to-bin-chars-aux n acc) → *
Function:
(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))))))