add-suffix-to-fn-or-const

(in-package "ACL2")

(define add-suffix-to-fn-or-const
  ((name symbolp) (suffix stringp))
  :returns (new-name symbolp)
  :parents (std/system)
  :short "Add a suffix to a function or constant name."
  :long (topstring (p "This is related to the built-in functions
     @(tsee add-suffix) and @(tsee add-suffix-to-fn).
     If the argument symbol starts and ends with @('*'),
     it is considered a constant name
     and the suffix is added just before the ending @('*'),
     so that the resulting symbol is still a constant name.
     Otherwise, the argument symbol is considered a function name
     and @(tsee add-suffix-to-fn) is used."))
  (let* ((s (symbol-name name)) (len (length s)))
    (cond ((and (not (= len 0))
         (eql (char s 0) #\*)
         (eql (char s (1- len)) #\*)) (if (equal (symbol-package-name name) *main-lisp-package-name*)
          (intern (concatenate 'string (subseq s 0 (1- len)) suffix "*")
            "ACL2")
          (intern-in-package-of-symbol (concatenate 'string (subseq s 0 (1- len)) suffix "*")
            name)))
      (t (add-suffix-to-fn name suffix)))))