		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-match-pred

Name of the <prefix>-matchp predicate.

Signature
(deftreeops-match-pred prefix) → pred
Arguments: prefix — Guard (common-lisp::symbolp prefix).
Returns: pred — Type (common-lisp::symbolp pred).

Definitions and Theorems

Function: deftreeops-match-pred

(defun deftreeops-match-pred (prefix)
  (declare (xargs :guard (common-lisp::symbolp prefix)))
  (let ((__function__ 'deftreeops-match-pred))
    (declare (ignorable __function__))
    (add-suffix-to-fn prefix "-MATCHP")))

Theorem: symbolp-of-deftreeops-match-pred

(defthm symbolp-of-deftreeops-match-pred
  (b* ((pred (deftreeops-match-pred prefix)))
    (common-lisp::symbolp pred))
  :rule-classes :rewrite)