		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-autohyps

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

Definitions and Theorems

Function: svtv-autohyps

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