		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Defsvtv-default-names

Signature
(defsvtv-default-names vars) → *

Definitions and Theorems

Function: defsvtv-default-names

(defun defsvtv-default-names (vars)
  (declare (xargs :guard t))
  (let ((__function__ 'defsvtv-default-names))
    (declare (ignorable __function__))
    (if (atom vars)
        nil
      (cons (cons (car vars)
                  (cons (cons 'quote (cons (car vars) 'nil))
                        'nil))
            (defsvtv-default-names (cdr vars))))))