		Search-engine friendly clone of the ACL2 documentation.

Fresh-namep

Chk-fresh-namep

Check whether name is a legal new name.

Signature
(chk-fresh-namep name type ctx wrld state) → (mv erp val state)
Arguments: name — Guard (symbolp name).; wrld — Guard (plist-worldp wrld).

Returns an error triple (mv erp val state) where erp is nil if and only if name is a legal new name, and val is irrelevant. If erp is not nil, then an explanatory error message is printed.

For more information about legality of new names see fresh-namep-msg, which returns an error triple, (mv nil msg/nil state). When non-nil, the value msg/nil provides the message printed by chk-fresh-namep.

Definitions and Theorems

Function: chk-fresh-namep

(defun chk-fresh-namep (name type ctx wrld state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (declare
  (xargs
      :guard
      (member-eq type
                 '(function macro
                            const stobj constrained-function nil))))
 (let ((__function__ 'chk-fresh-namep))
   (declare (ignorable __function__))
   (er-let* ((msg (fresh-namep-msg name type wrld state)))
            (cond (msg (er soft ctx "~@0" msg))
                  (t (value nil))))))