Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Std/lists
Std/alists
Obags
Std/util
Std/strings
Std/io
Std/osets
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-extensions
Std/system/constant-queries
Std/typed-lists
Std/bitsets
Std/testing
Std/typed-alists
Std/stobjs
Std-extensions
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Std/system/event-name-queries
Fresh-namep
Utilities to check the freshness of event names.
Subtopics
Fresh-namep-msg
Return either
nil
or a message indicating why the name is not a legal new name.
Fresh-namep-msg-weak
Return either
nil
or a message indicating why the name is not a legal new name.
Chk-fresh-namep
Check whether name is a legal new name.
Fresh-name-listp-msg-weak
Lift
fresh-namep-msg-weak
to lists.