add-suffix-to-fn-lst

(in-package "ACL2")

(define add-suffix-to-fn-lst
  ((syms symbol-listp) (suffix stringp))
  :returns (new-syms symbol-listp)
  :parents (std/system)
  :short "Apply @(tsee add-suffix-to-fn) to a list of symbols,
          all with the same suffix."
  (cond ((endp syms) nil)
    (t (cons (add-suffix-to-fn (car syms) suffix)
        (add-suffix-to-fn-lst (cdr syms) suffix))))
  ///
  (defret len-of-add-suffix-to-fn-lst
    (equal (len new-syms) (len syms))))