		Search-engine friendly clone of the ACL2 documentation.

Stv-run

Stv-print-alist

Dumb printing utility. X is expected to be an alist binding symbols to values. We print them out hexified and indented in a nice way.

Signature
(stv-print-alist x) → *

Definitions and Theorems

Function: stv-print-alist

(defun stv-print-alist (x)
 (declare (xargs :guard t))
 (let ((__function__ 'stv-print-alist))
   (declare (ignorable __function__))
   (b*
    (((when (atom x)) nil)
     ((unless (consp (car x)))
      (raise
           "Malformed alist: Entry ~x0 is not a (key . val) pair.~%"
           (car x)))
     ((cons key val) (car x))
     ((unless (symbolp key))
      (raise "Malformed alist: name is not a symbolp.~%"
             (car x)))
     (- (cw "  ~s0:~t1~s2~%"
            key 20 (str::hexify val))))
    (stv-print-alist (cdr x)))))