		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-input-processing

Defdefparse-process-package

Process the :package input.

Signature
(defdefparse-process-package package ctx state) → (mv erp pkg-wit state)
Arguments: ctx — Guard (ctxp ctx).
Returns: pkg-wit — Type (common-lisp::symbolp pkg-wit).

If successful, return the witness of the package.

Definitions and Theorems

Function: defdefparse-process-package

(defun defdefparse-process-package (package ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (ctxp ctx)))
 (let ((__function__ 'defdefparse-process-package))
  (declare (ignorable __function__))
  (b*
   (((er &)
     (ensure-value-is-string$ package "The :PACKAGE input" t nil))
    (known-packages (known-packages+ state))
    ((unless (member-equal package known-packages))
     (er-soft+
      ctx t nil
      "The :PACKAGE input ~x0 must be ~
                   among the known packages ~&1."
      package known-packages))
    ((when (equal package ""))
     (value (raise "Internal error: empty package name."))))
   (value (pkg-witness package)))))

Theorem: symbolp-of-defdefparse-process-package.pkg-wit

(defthm symbolp-of-defdefparse-process-package.pkg-wit
  (b* (((mv acl2::?erp ?pkg-wit acl2::?state)
        (defdefparse-process-package package ctx state)))
    (common-lisp::symbolp pkg-wit))
  :rule-classes :rewrite)