Lift a package from the current ACL2 environment to the meta level.
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.
(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)))))
(defthm packagep-of-lift-package (b* ((package (lift-package name))) (packagep package)) :rule-classes :rewrite)