		Search-engine friendly clone of the ACL2 documentation.

Std/system

Add-suffix-to-fn-lst

Apply add-suffix-to-fn to a list of symbols, all with the same suffix.

Signature
(add-suffix-to-fn-lst syms suffix) → new-syms
Arguments: syms — Guard (symbol-listp syms).; suffix — Guard (stringp suffix).
Returns: new-syms — Type (symbol-listp new-syms).

Definitions and Theorems

Function: add-suffix-to-fn-lst

(defun add-suffix-to-fn-lst (syms suffix)
       (declare (xargs :guard (and (symbol-listp syms)
                                   (stringp suffix))))
       (let ((__function__ 'add-suffix-to-fn-lst))
            (declare (ignorable __function__))
            (cond ((endp syms) nil)
                  (t (cons (add-suffix-to-fn (car syms) suffix)
                           (add-suffix-to-fn-lst (cdr syms)
                                                 suffix))))))

Theorem: symbol-listp-of-add-suffix-to-fn-lst

(defthm symbol-listp-of-add-suffix-to-fn-lst
        (b* ((new-syms (add-suffix-to-fn-lst syms suffix)))
            (symbol-listp new-syms))
        :rule-classes :rewrite)

Theorem: len-of-add-suffix-to-fn-lst

(defthm len-of-add-suffix-to-fn-lst
        (b* ((?new-syms (add-suffix-to-fn-lst syms suffix)))
            (equal (len new-syms) (len syms))))