		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

In-home-package-p

Signature
(in-home-package-p sym config) → *
Arguments: sym — Guard (symbolp sym).; config — Guard (printconfig-p config).

Definitions and Theorems

Function: in-home-package-p$inline

(defun in-home-package-p$inline (sym config)
  (declare (xargs :guard (and (symbolp sym)
                              (printconfig-p config))))
  (let ((acl2::__function__ 'in-home-package-p))
    (declare (ignorable acl2::__function__))
    (b* ((pkg-name (symbol-package-name sym))
         (home-pkg-sym (printconfig->home-package config)))
      (or (equal (symbol-package-name home-pkg-sym)
                 pkg-name)
          (eq sym
              (intern-in-package-of-symbol (symbol-name sym)
                                           home-pkg-sym))))))