• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
      • Mutual-recursion
      • Memoize
      • Mbe
      • Io
      • Defpkg
      • Apply$
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Defmacro
      • Loop$-primer
      • Fast-alists
      • Defconst
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Efficiency
      • Irrelevant-formals
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
        • Defpkg
        • *ACL2-exports*
        • Package-reincarnation-import-restrictions
        • *common-lisp-symbols-from-main-lisp-package*
        • Pkg-imports
        • Hidden-death-package
        • Symbol-package-name
        • Intern
        • Working-with-packages
        • Intern-in-package-of-symbol
        • ACL2-user
        • Packages-for-generated-symbols
        • In-package
        • Pkg-witness
        • *ACL2-system-exports*
        • Intern$
        • Sharp-bang-reader
        • Managing-ACL2-packages
        • Hidden-defpkg
      • Oracle-eval
      • Defmacro-untouchable
      • <<
      • Primitive
      • Revert-world
      • Unmemoize
      • Set-duplicate-keys-action
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Fake-oracle-eval
      • Defopen
      • Sleep
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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.

Package-reincarnation-import-restrictions

Re-defining undone defpkgs

*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

Hidden-death-package

Handling defpkg events that are local

Symbol-package-name

The name of the package of a symbol (a string)

Intern

Create a new symbol in a given package

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

Packages-for-generated-symbols

Convention for packages of generated symbols

In-package

Select current package

Pkg-witness

Return a specific symbol in the indicated 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