		Search-engine friendly clone of the ACL2 documentation.

Stv-easy-bindings

Stv-easy-bindings-inside-mix

Signature
(stv-easy-bindings-inside-mix x stv) → *
Arguments: x — Some arguments inside of a :mix.; stv — Guard (processed-stv-p stv).

Definitions and Theorems

Function: stv-easy-bindings-inside-mix

(defun stv-easy-bindings-inside-mix (x stv)
 (declare (xargs :guard (processed-stv-p stv)))
 (let ((__function__ 'stv-easy-bindings-inside-mix))
  (declare (ignorable __function__))
  (cond
   ((atom x) nil)
   ((symbolp (car x))
    (cons (cons ':nat
                (cons (car x)
                      (cons (stv-in->width (car x) stv)
                            'nil)))
          (stv-easy-bindings-inside-mix (cdr x)
                                        stv)))
   (t
    (raise
     "Inside a :mix you can only have symbols (the names of stv ~
                 inputs), so ~x0 is illegal."
     (car x))))))