Construct a paired 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).
(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))))
(defthm symbolp-of-make-paired-name (b* ((name (make-paired-name first-name second-name pkg-from wrld))) (symbolp name)) :rule-classes :rewrite)