		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-input-processing

Deftreeops-process-prefix

Process the :prefix input.

Signature
(deftreeops-process-prefix prefix) → (mv erp prefix)
Returns: prefix — Type (common-lisp::symbolp prefix).

Definitions and Theorems

Function: deftreeops-process-prefix

(defun deftreeops-process-prefix (prefix)
  (declare (xargs :guard t))
  (let ((__function__ 'deftreeops-process-prefix))
    (declare (ignorable __function__))
    (b* (((reterr) nil)
         ((unless (common-lisp::symbolp prefix))
          (reterr (msg "The :PREFIX input ~x0 must be a symbol."
                       prefix))))
      (retok prefix))))

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

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