		Search-engine friendly clone of the ACL2 documentation.

Packages

Lift-package

Lift a package from the current ACL2 environment to the meta level.

Signature
(lift-package name) → package
Arguments: name — Guard (stringp name).
Returns: package — Type (packagep package).

This must be used only on package names that are currently known. Otherwise, pkg-imports will cause an error.

We retrieve the imports of the package (a list of symbols), we lift them to the meta level, and we construct a package with the given name and lifted imports.

Definitions and Theorems

Function: lift-package

(defun lift-package (name)
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'lift-package))
    (declare (ignorable __function__))
    (b* ((imports (pkg-imports name)))
      (make-package :name name
                    :imports (lift-symbol-list imports)))))

Theorem: packagep-of-lift-package

(defthm packagep-of-lift-package
  (b* ((package (lift-package name)))
    (packagep package))
  :rule-classes :rewrite)