		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Deftrans-get-args

Gets arg names from a define-style arg list.

Signature
(deftrans-get-args args) → *
Arguments: args — Guard (true-listp args).

Definitions and Theorems

Function: deftrans-get-args

(defun deftrans-get-args (args)
  (declare (xargs :guard (true-listp args)))
  (let ((__function__ 'deftrans-get-args))
    (declare (ignorable __function__))
    (if (endp args)
        nil
      (cons (if (consp (first args))
                (car (first args))
              (first args))
            (deftrans-get-args (rest args))))))