		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-default-update-names

Default names of the iterated argument update functions.

Signature
(defarbrec-default-update-names x1...xn$ fn$) → names
Arguments: x1...xn$ — Guard (symbol-listp x1...xn$).; fn$ — Guard (symbolp fn$).
Returns: names — Type (symbol-listp names).

These are used when the :update-names input is nil. They are as described in the documentation.

Definitions and Theorems

Function: defarbrec-default-update-names-aux

(defun defarbrec-default-update-names-aux (xi...xn$ fn$)
 (declare (xargs :guard (and (symbol-listp xi...xn$)
                             (symbolp fn$))))
 (let ((__function__ 'defarbrec-default-update-names-aux))
  (declare (ignorable __function__))
  (if (endp xi...xn$)
      nil
   (cons
        (add-suffix-to-fn fn$
                          (str::cat "-" (symbol-name (car xi...xn$))
                                    "*"))
        (defarbrec-default-update-names-aux (cdr xi...xn$)
                                            fn$)))))

Theorem: symbol-listp-of-defarbrec-default-update-names-aux

(defthm symbol-listp-of-defarbrec-default-update-names-aux
  (b* ((names (defarbrec-default-update-names-aux xi...xn$ fn$)))
    (symbol-listp names))
  :rule-classes :rewrite)

Function: defarbrec-default-update-names

(defun defarbrec-default-update-names (x1...xn$ fn$)
  (declare (xargs :guard (and (symbol-listp x1...xn$)
                              (symbolp fn$))))
  (let ((__function__ 'defarbrec-default-update-names))
    (declare (ignorable __function__))
    (defarbrec-default-update-names-aux x1...xn$ fn$)))

Theorem: symbol-listp-of-defarbrec-default-update-names

(defthm symbol-listp-of-defarbrec-default-update-names
  (b* ((names (defarbrec-default-update-names x1...xn$ fn$)))
    (symbol-listp names))
  :rule-classes :rewrite)