		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-fresh-defsurj-name-with-*s-suffix

Suffix a name with as many *s as needed to make it a valid name for a new defsurj.

Signature
(expdata-fresh-defsurj-name-with-*s-suffix name wrld) → fresh-name
Arguments: name — Guard (symbolp name).; wrld — Guard (plist-worldp wrld).
Returns: fresh-name — A symbolp.

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 *s are added.

Definitions and Theorems

Function: expdata-fresh-defsurj-name-with-*s-suffix-aux

(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: expdata-fresh-defsurj-name-with-*s-suffix

(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))))