Defstv

Stv-autohyps

Generate the body for an STV's autohyps macro.

Signature
(stv-autohyps stv) → *
Arguments: stv — Guard (processed-stv-p stv).

Definitions and Theorems

Function: stv-autohyps

(defun stv-autohyps (stv)
  (declare (xargs :guard (processed-stv-p stv)))
  (let ((__function__ 'stv-autohyps))
    (declare (ignorable __function__))
    (b* ((ins (stv->ins stv))
         ((unless (symbol-listp ins))
          (raise "Non-symbol inputs?")))
      (cons 'and
            (stv-autohyps-aux ins stv)))))

Subtopics

Stv-autohyps-aux