		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)