• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
    • Std/lists
    • Omaps
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
      • Fresh-logical-name-with-$s-suffix
      • Irrelevant-formals-info
      • Std/system/function-queries
      • Std/system/term-queries
      • Std/system/term-transformations
      • Std/system/enhanced-utilities
      • Install-not-normalized-event
      • Install-not-normalized-event-lst
      • Std/system/term-function-recognizers
      • Genvar$
      • Std/system/event-name-queries
        • Logic-function-namep
        • Function-namep
        • Theorem-symbolp
        • Macro-symbolp
        • Logical-name-listp
        • Constant-symbolp
        • Theorem-symbol-listp
        • Theorem-name-listp
        • Macro-symbol-listp
        • Macro-name-listp
        • Function-symbol-listp
        • Function-name-listp
        • Theorem-namep
        • Macro-namep
        • Constant-namep
        • Fresh-namep
          • Fresh-namep-msg
          • Fresh-namep-msg-weak
          • Chk-fresh-namep
          • Fresh-name-listp-msg-weak
        • Std/system/function-symbolp
      • Pseudo-tests-and-call-listp
      • Maybe-pseudo-event-formp
      • Add-suffix-to-fn-or-const
      • Chk-irrelevant-formals-ok
      • Table-alist+
      • Pseudo-tests-and-callp
      • Add-suffix-to-fn-or-const-lst
      • Known-packages+
      • Add-suffix-to-fn-lst
      • Unquote-term
      • Event-landmark-names
      • Add-suffix-lst
      • Std/system/theorem-queries
      • Unquote-term-list
      • Std/system/macro-queries
      • Pseudo-command-landmark-listp
      • Install-not-normalized$
      • Pseudo-event-landmark-listp
      • Known-packages
      • Std/system/partition-rest-and-keyword-args
      • Rune-enabledp
      • Rune-disabledp
      • Included-books
      • Std/system/pseudo-event-formp
      • Std/system/plist-worldp-with-formals
      • Std/system/w
      • Std/system/geprops
      • Std/system/arglistp
      • Std/system/constant-queries
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Fresh-namep
• Fresh-namep-msg-weak

Fresh-name-listp-msg-weak

Lift fresh-namep-msg-weak to lists.

Signature

(fresh-name-listp-msg-weak names type wrld) → msg/nil

Arguments

names — Guard (symbol-listp names).

wrld — Guard (plist-worldp wrld).

Returns

msg/nil — A message (see msg) or nil.

As soon as one name in the list fails the test, stop and return the message. If all the names are fresh, return nil.

Definitions and Theorems

Function: fresh-name-listp-msg-weak

(defun fresh-name-listp-msg-weak (names type wrld)
 (declare (xargs :guard (and (symbol-listp names)
                             (plist-worldp wrld))))
 (declare
  (xargs
      :guard
      (member-eq type
                 '(function macro
                            const stobj constrained-function nil))))
 (let ((__function__ 'fresh-name-listp-msg-weak))
   (declare (ignorable __function__))
   (cond ((endp names) nil)
         (t (or (fresh-namep-msg-weak (car names)
                                      type wrld)
                (fresh-name-listp-msg-weak (cdr names)
                                           type wrld))))))