		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-extra-args-to-names

Map the :extra-args input to a list of the names of the arguments.

Signature
(deffold-map-extra-args-to-names extra-args) → names
Arguments: extra-args — Guard (true-listp extra-args).
Returns: names — Type (true-listp names).

Definitions and Theorems

Function: deffold-map-extra-args-to-names

(defun deffold-map-extra-args-to-names (extra-args)
  (declare (xargs :guard (true-listp extra-args)))
  (let ((__function__ 'deffold-map-extra-args-to-names))
    (declare (ignorable __function__))
    (b* (((when (endp extra-args)) nil)
         (extra-arg (car extra-args))
         (name (if (atom extra-arg)
                   extra-arg
                 (car extra-arg)))
         (names (deffold-map-extra-args-to-names (cdr extra-args))))
      (cons name names))))

Theorem: true-listp-of-deffold-map-extra-args-to-names

(defthm true-listp-of-deffold-map-extra-args-to-names
  (b* ((names (deffold-map-extra-args-to-names extra-args)))
    (true-listp names))
  :rule-classes :rewrite)