Defstv

Stv-autoins

Generate the body for an STV's autoins macro.

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

Definitions and Theorems

Function: stv-autoins

(defun stv-autoins (stv)
  (declare (xargs :guard (processed-stv-p stv)))
  (let ((__function__ 'stv-autoins))
    (declare (ignorable __function__))
    (cons 'list
          (stv-autoins-aux (stv->ins stv)))))

Subtopics

Stv-autoins-aux