Suffix a name with as many
(expdata-fresh-defsurj-name-with-*s-suffix name wrld) → fresh-name
A name is valid for a new defsurj if it is not already a key in the defsurj table.
We use this function for generating local defsurjs.
If the input name is already valid, no
Function:
(defun expdata-fresh-defsurj-name-with-*s-suffix-aux (name table) (declare (xargs :guard (and (symbolp name) (alistp table)))) (let ((__function__ 'expdata-fresh-defsurj-name-with-*s-suffix-aux)) (declare (ignorable __function__)) (if (consp (assoc-eq name table)) (expdata-fresh-defsurj-name-with-*s-suffix-aux (packn-pos (list name '*) name) table) name)))
Function:
(defun expdata-fresh-defsurj-name-with-*s-suffix (name wrld) (declare (xargs :guard (and (symbolp name) (plist-worldp wrld)))) (let ((__function__ 'expdata-fresh-defsurj-name-with-*s-suffix)) (declare (ignorable __function__)) (b* ((table (table-alist *defmapping-table-name* wrld) )) (expdata-fresh-defsurj-name-with-*s-suffix-aux name table))))