		Search-engine friendly clone of the ACL2 documentation.

Stv-autobinds

Stv-autobinds-aux

Signature
(stv-autobinds-aux ins stv) → *
Arguments: ins — Guard (symbol-listp ins).; stv — Guard (processed-stv-p stv).

Definitions and Theorems

Function: stv-autobinds-aux

(defun stv-autobinds-aux (ins stv)
  (declare (xargs :guard (and (symbol-listp ins)
                              (processed-stv-p stv))))
  (let ((__function__ 'stv-autobinds-aux))
    (declare (ignorable __function__))
    (if (atom ins)
        nil
      (cons (cons ':nat
                  (cons (car ins)
                        (cons (stv-in->width (car ins) stv)
                              'nil)))
            (stv-autobinds-aux (cdr ins) stv)))))