RosettaCodeData/Task/Binary-digits/ACL2/binary-digits.acl2

(include-book "arithmetic-3/top" :dir :system)

(defun bin-string-r (x)
   (if (zp x)
       ""
       (string-append
        (bin-string-r (floor x 2))
        (if (= 1 (mod x 2))
            "1"
            "0"))))

(defun bin-string (x)
   (if (zp x)
       "0"
       (bin-string-r x)))