Pretty-print a direct numeric value notation.
(pretty-print-num-val-direct nats base) → string
The parameters of this pretty-printing function are the components of the direct numeric value notation.
Function:
(defun pretty-print-num-val-direct-aux (nats base) (declare (xargs :guard (and (nat-listp nats) (num-base-p base)))) (let ((__function__ 'pretty-print-num-val-direct-aux)) (declare (ignorable __function__)) (cond ((endp nats) "") ((endp (cdr nats)) (pretty-print-number (car nats) base)) (t (str::cat (pretty-print-number (car nats) base) "." (pretty-print-num-val-direct-aux (cdr nats) base))))))
Theorem:
(defthm stringp-of-pretty-print-num-val-direct-aux (b* ((string (pretty-print-num-val-direct-aux nats base))) (common-lisp::stringp string)) :rule-classes :rewrite)
Function:
(defun pretty-print-num-val-direct (nats base) (declare (xargs :guard (and (nat-listp nats) (num-base-p base)))) (let ((__function__ 'pretty-print-num-val-direct)) (declare (ignorable __function__)) (str::cat (pretty-print-num-base base) (pretty-print-num-val-direct-aux nats base))))
Theorem:
(defthm stringp-of-pretty-print-num-val-direct (b* ((string (pretty-print-num-val-direct nats base))) (common-lisp::stringp string)) :rule-classes :rewrite)