		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-autobinds

Signature
(svtv-autobinds x) → *
Arguments: x — Guard (svtv-p x).

Definitions and Theorems

Function: svtv-autobinds

(defun svtv-autobinds (x)
  (declare (xargs :guard (svtv-p x)))
  (let ((__function__ 'svtv-autobinds))
    (declare (ignorable __function__))
    (cons 'gl::auto-bindings
          (b* ((inmap (svtv->inmap x)))
            (with-fast-alist inmap
                             (svtv-autobinds-aux (svtv->inmasks x)
                                                 inmap))))))