		Search-engine friendly clone of the ACL2 documentation.

Std/system

Add-suffix-to-fn-or-const

Add a suffix to a function or constant name.

Signature
(add-suffix-to-fn-or-const name suffix) → new-name
Arguments: name — Guard (symbolp name).; suffix — Guard (stringp suffix).
Returns: new-name — Type (symbolp new-name).

This is related to the built-in functions add-suffix and 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 add-suffix-to-fn is used.

Definitions and Theorems

Function: add-suffix-to-fn-or-const

(defun add-suffix-to-fn-or-const (name suffix)
  (declare (xargs :guard (and (symbolp name) (stringp suffix))))
  (let ((__function__ 'add-suffix-to-fn-or-const))
    (declare (ignorable __function__))
    (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))))))

Theorem: symbolp-of-add-suffix-to-fn-or-const

(defthm symbolp-of-add-suffix-to-fn-or-const
  (b* ((new-name (add-suffix-to-fn-or-const name suffix)))
    (symbolp new-name))
  :rule-classes :rewrite)