Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Hons-and-memoization
Events
History
Parallelism
Programming
Defun
Declare
Stobj
State
Memoize
Mbe
Io
Apply$
System-utilities
Defpkg
Mutual-recursion
Programming-with-state
Arrays
Characters
Loop$
Time$
Fast-alists
Defmacro
Defconst
Guard
Evaluation
Equality-variants
Compilation
Hons
ACL2-built-ins
Advanced-features
Set-check-invariant-risk
Developers-guide
Numbers
Irrelevant-formals
Efficiency
Introduction-to-programming-in-ACL2-for-those-who-know-lisp
Redefining-programs
Lists
Invariant-risk
Errors
Defabbrev
Conses
Alists
Set-register-invariant-risk
Program-wrapper
Strings
Get-internal-time
Basics
Packages
Defpkg
*ACL2-exports*
*common-lisp-symbols-from-main-lisp-package*
Pkg-imports
Symbol-package-name
Intern
Hidden-death-package
Working-with-packages
Intern-in-package-of-symbol
ACL2-user
Package-reincarnation-import-restrictions
Packages-for-generated-symbols
Pkg-witness
In-package
*ACL2-system-exports*
Intern$
Sharp-bang-reader
Managing-ACL2-packages
Hidden-defpkg
System-attachments
Defmacro-untouchable
Primitive
<<
Revert-world
Set-duplicate-keys-action
Unmemoize
Symbols
Def-list-constructor
Easy-simplify-term
Defiteration
Defopen
Sleep
Real
ACL2-tutorial
Debugging
Miscellaneous
Output-controls
Built-in-theorems
Macros
Interfacing-tools
About-ACL2
Interfacing-tools
Hardware-verification
Software-verification
Testing-utilities
Math
Programming
Packages
Collections of symbols that act as namespaces.
Packages are collections of symbols. They can be used to avoid name conflicts when working on large ACL2 projects. See
working-with-packages
for the best practices in setting up and using packages.
Subtopics
Defpkg
Define a new symbol package
*ACL2-exports*
Symbols that are often imported into new
packages
to provide easy access to ACL2 functionality.
*common-lisp-symbols-from-main-lisp-package*
Symbols that are often imported into new packages to provide easy access to Common Lisp functionality.
Pkg-imports
List of symbols imported into a given package
Symbol-package-name
The name of the package of a symbol (a string)
Intern
Create a new symbol in a given package
Hidden-death-package
Handling
defpkg
events
that are
local
Working-with-packages
How to set up new package and portcullis files.
Intern-in-package-of-symbol
Create a symbol with a given name
ACL2-user
A package the ACL2 user may prefer
Package-reincarnation-import-restrictions
Re-defining undone
defpkg
s
Packages-for-generated-symbols
Convention for packages of generated symbols
Pkg-witness
Return a specific symbol in the indicated package
In-package
Select current package
*ACL2-system-exports*
An extension of
*ACL2-exports*
that includes the names of many system-level ACL2 functions.
Intern$
Create a new symbol in a given package
Sharp-bang-reader
Package prefix that is not restricted to symbols
Managing-ACL2-packages
User-contributed documentation on packages
Hidden-defpkg
Handling defpkg events that are local