		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-input-processing

Defdefparse-process-prefix

Process the :prefix input.

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

Definitions and Theorems

Function: defdefparse-process-prefix

(defun defdefparse-process-prefix (prefix ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (ctxp ctx)))
 (let ((__function__ 'defdefparse-process-prefix))
  (declare (ignorable __function__))
  (b* (((er &)
        (ensure-value-is-symbol$ prefix "The :PREFIX input" t nil)))
    (value prefix))))

Theorem: symbolp-of-defdefparse-process-prefix.prefix

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