		Search-engine friendly clone of the ACL2 documentation.

Lifting

Current-package+

Logic-friendly wrapper of the built-in current-package.

Signature
(current-package+ state) → package
Returns: package — Type (stringp package).

This belongs to a more general library.

Definitions and Theorems

Function: current-package+

(defun current-package+ (state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'current-package+))
   (declare (ignorable __function__))
   (b*
     ((package (current-package state))
      ((unless (and (stringp package)
                    (not (equal package ""))))
       (raise "Internal error: current package ~x0 is not a string."
              package)
       "."))
     package)))

Theorem: stringp-of-current-package+

(defthm stringp-of-current-package+
  (b* ((package (current-package+ state)))
    (stringp package))
  :rule-classes :rewrite)

Theorem: current-package+-not-empty

(defthm current-package+-not-empty
  (b* ((common-lisp::?package (current-package+ state)))
    (not (equal package ""))))