		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

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

Signature
(expdata-fresh-defsurj-name-with-*s-suffix-aux name table) → fresh-name
Arguments: name — Guard (symbolp name).; table — Guard (alistp table).

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