		Search-engine friendly clone of the ACL2 documentation.

Binary

Binify

Convert numbers into readable binary strings.

(binify x) is identical to hexify except that it produces binary output instead of hex output.

Definitions and Theorems

Function: binify

(defun binify (x)
 (declare (xargs :guard t))
 (cond
  ((integerp x)
   (b*
    ((xsign (< x 0))
     (xabs (abs x))
     (chars (explode-atom xabs 2))
     (nice-chars
       (list*
            #\# #\u #\b
            (append (and xsign '(#\-))
                    (cons (first chars)
                          (insert-underscores (nthcdr 1 chars)))))))
    (implode nice-chars)))
  ((symbolp x) (symbol-name x))
  ((stringp x) x)
  (t (prog2$ (er hard? 'binify
                 "Unexpected argument ~x0.~%" x)
             ""))))