		Search-engine friendly clone of the ACL2 documentation.

Fresh-namep

Fresh-namep-msg-weak

Return either nil or a message indicating why the name is not a legal new name.

Signature
(fresh-namep-msg-weak name type wrld) → msg/nil
Arguments: name — Guard (symbolp name).; wrld — Guard (plist-worldp wrld).
Returns: msg/nil — A message (see msg) or nil.

This helper function for fresh-namep-msg avoids the ``virginity'' check ensuring that the name is not already defined in raw Lisp. See fresh-namep-msg.

Definitions and Theorems

Function: fresh-namep-msg-weak

(defun fresh-namep-msg-weak (name type wrld)
 (declare (xargs :guard (and (symbolp name)
                             (plist-worldp wrld))))
 (declare
  (xargs
      :guard
      (member-eq type
                 '(function macro
                            const stobj constrained-function nil))))
 (let ((__function__ 'fresh-namep-msg-weak))
  (declare (ignorable __function__))
  (flet
   ((not-new-namep-msg
     (name wrld)
     (let ((old-type (logical-name-type name wrld t)))
      (cond
       (old-type
            (msg "~x0 is already the name for a ~s1."
                 name
                 (case old-type
                   (function "function")
                   (macro "macro")
                   (const "constant")
                   (stobj "stobj")
                   (constrained-function "constrained function")
                   (theorem "theorem"))))
       (t
        (msg
         "~x0 has properties in the world; it is ~
                                      not a new name."
         name))))))
   (cond ((mv-let (ctx msg)
                  (chk-all-but-new-name-cmp name 'fresh-namep-msg
                                            type wrld)
            (and ctx msg)))
         ((not (new-namep name wrld))
          (not-new-namep-msg name wrld))
         (t (case type
              (const (and (not (legal-constantp name))
                          (msg "~x0 is not a legal constant name."
                               name)))
              (stobj (and (not (new-namep (the-live-var name) wrld))
                          (not-new-namep-msg (the-live-var name)
                                             wrld)))
              (t nil)))))))

Subtopics

Fresh-name-listp-msg-weak: Lift fresh-namep-msg-weak to lists.