		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-autoins

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

Definitions and Theorems

Function: svtv-autoins

(defun svtv-autoins (x)
 (declare (xargs :guard (svtv-p x)))
 (let ((__function__ 'svtv-autoins))
  (declare (ignorable __function__))
  (cons
     'list
     (reverse (b* ((inmap (svtv->inmap x)))
                (with-fast-alist inmap
                                 (svtv-autoins-aux (svtv->inmasks x)
                                                   inmap)))))))