		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))))