Defstv

Stv-autobinds

Generate the body for an STV's autobinds macro.

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

Definitions and Theorems

Function: stv-autobinds

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

Subtopics

Stv-autobinds-aux