		Search-engine friendly clone of the ACL2 documentation.

Stv-autoins

Stv-autoins-aux

Signature
(stv-autoins-aux ins) → *

Definitions and Theorems

Function: stv-autoins-aux

(defun stv-autoins-aux (ins)
  (declare (xargs :guard t))
  (let ((__function__ 'stv-autoins-aux))
    (declare (ignorable __function__))
    (if (atom ins)
        nil
      (cons (cons 'cons
                  (cons (cons 'quote (cons (car ins) 'nil))
                        (cons (car ins) 'nil)))
            (stv-autoins-aux (cdr ins))))))