		Search-engine friendly clone of the ACL2 documentation.

Paired-names

Make-paired-name

Construct a paired name.

Signature
(make-paired-name first-name second-name pkg-from wrld) → name
Arguments: first-name — Guard (symbolp first-name).; second-name — Guard (symbolp second-name).; wrld — Guard (plist-worldp wrld).
Returns: name — Type (symbolp name).

The resulting name consists of the given first and second names, separated by the current separator. An additional argument says whether the package of the resulting name should be the same as the first or second name (immaterial if the first and second names are in the same package).

Definitions and Theorems

Function: make-paired-name

(defun make-paired-name (first-name second-name pkg-from wrld)
 (declare (type (integer 1 2) pkg-from))
 (declare (xargs :guard (and (symbolp first-name)
                             (symbolp second-name)
                             (plist-worldp wrld))))
 (let ((__function__ 'make-paired-name))
   (declare (ignorable __function__))
   (b* ((first-chars (explode (symbol-name first-name)))
        (second-chars (explode (symbol-name second-name)))
        (separator-chars (explode (get-paired-name-separator wrld)))
        (name-chars (append first-chars
                            separator-chars second-chars))
        (pkg-symbol (case pkg-from
                      (1 first-name)
                      (2 second-name)
                      (t (impossible)))))
     (intern-in-package-of-symbol (implode name-chars)
                                  pkg-symbol))))

Theorem: symbolp-of-make-paired-name

(defthm symbolp-of-make-paired-name
  (b*
    ((name (make-paired-name first-name second-name pkg-from wrld)))
    (symbolp name))
  :rule-classes :rewrite)