		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-octdig/uscore-list

Pretty-print a list of octal digits and underscores.

Signature
(print-octdig/uscore-list dus) → part
Arguments: dus — Guard (octdig/uscore-listp dus).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: print-octdig/uscore-list

(defun print-octdig/uscore-list (dus)
  (declare (xargs :guard (octdig/uscore-listp dus)))
  (let ((__function__ 'print-octdig/uscore-list))
    (declare (ignorable __function__))
    (cond ((endp dus) "")
          (t (msg "~@0~@1" (print-octdig/uscore (car dus))
                  (print-octdig/uscore-list (cdr dus)))))))

Theorem: msgp-of-print-octdig/uscore-list

(defthm msgp-of-print-octdig/uscore-list
  (b* ((part (print-octdig/uscore-list dus)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: print-octdig/uscore-list-of-octdig/uscore-list-fix-dus

(defthm print-octdig/uscore-list-of-octdig/uscore-list-fix-dus
  (equal (print-octdig/uscore-list (octdig/uscore-list-fix dus))
         (print-octdig/uscore-list dus)))

Theorem: print-octdig/uscore-list-octdig/uscore-list-equiv-congruence-on-dus

(defthm
 print-octdig/uscore-list-octdig/uscore-list-equiv-congruence-on-dus
 (implies (octdig/uscore-list-equiv dus dus-equiv)
          (equal (print-octdig/uscore-list dus)
                 (print-octdig/uscore-list dus-equiv)))
 :rule-classes :congruence)