		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-fresh-defiso-name-with-*s-suffix

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

Signature
(isodata-fresh-defiso-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 defiso if it is not already a key in the defiso table.

We use this function for generating local defisos.

If the input name is already valid, no *s are added.

Definitions and Theorems

Function: isodata-fresh-defiso-name-with-*s-suffix-aux

(defun isodata-fresh-defiso-name-with-*s-suffix-aux (name table)
 (declare (xargs :guard (and (symbolp name) (alistp table))))
 (let ((__function__ 'isodata-fresh-defiso-name-with-*s-suffix-aux))
   (declare (ignorable __function__))
   (if (consp (assoc-eq name table))
       (isodata-fresh-defiso-name-with-*s-suffix-aux
            (packn-pos (list name '*) name)
            table)
     name)))

Function: isodata-fresh-defiso-name-with-*s-suffix

(defun isodata-fresh-defiso-name-with-*s-suffix (name wrld)
  (declare (xargs :guard (and (symbolp name)
                              (plist-worldp wrld))))
  (let ((__function__ 'isodata-fresh-defiso-name-with-*s-suffix))
    (declare (ignorable __function__))
    (b* ((table (table-alist *defmapping-table-name* wrld)
))
      (isodata-fresh-defiso-name-with-*s-suffix-aux name table))))