(nat-to-dec-string-size-fast x) → *
Function:
(defun nat-to-dec-string-size-fast (x) (declare (type (unsigned-byte 29) x)) (let ((acl2::__function__ 'nat-to-dec-string-size-fast)) (declare (ignorable acl2::__function__)) (mbe :logic (nat-to-dec-string-size-slow x) :exec (if (< x 10) 1 (the (unsigned-byte 29) (+ 1 (the (unsigned-byte 29) (nat-to-dec-string-size-fast (the (unsigned-byte 29) (truncate x 10))))))))))