		Search-engine friendly clone of the ACL2 documentation.

Grammar

Cst-matchp$

Signature
(cst-matchp$ abnf::tree abnf::elem) → abnf::yes/no
Arguments: abnf::tree — Guard (abnf::treep abnf::tree).; abnf::elem — Guard (abnf::elementp abnf::elem).
Returns: abnf::yes/no — Type (booleanp abnf::yes/no).

Definitions and Theorems

Function: cst-matchp$

(defun cst-matchp$ (abnf::tree abnf::elem)
 (declare (xargs :guard (and (abnf::treep abnf::tree)
                             (abnf::elementp abnf::elem))))
 (let ((__function__ 'cst-matchp$))
  (declare (ignorable __function__))
  (and
      (abnf::tree-terminatedp abnf::tree)
      (abnf::tree-match-element-p abnf::tree
                                  abnf::elem *all-grammar-rules*))))

Theorem: booleanp-of-cst-matchp$

(defthm booleanp-of-cst-matchp$
  (b* ((abnf::yes/no (cst-matchp$ abnf::tree abnf::elem)))
    (booleanp abnf::yes/no))
  :rule-classes :rewrite)

Theorem: cst-matchp$-of-tree-fix-tree

(defthm cst-matchp$-of-tree-fix-tree
  (equal (cst-matchp$ (abnf::tree-fix abnf::tree)
                      abnf::elem)
         (cst-matchp$ abnf::tree abnf::elem)))

Theorem: cst-matchp$-tree-equiv-congruence-on-tree

(defthm cst-matchp$-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv abnf::tree tree-equiv)
           (equal (cst-matchp$ abnf::tree abnf::elem)
                  (cst-matchp$ tree-equiv abnf::elem)))
  :rule-classes :congruence)

Theorem: cst-matchp$-of-element-fix-elem

(defthm cst-matchp$-of-element-fix-elem
  (equal (cst-matchp$ abnf::tree
                      (abnf::element-fix abnf::elem))
         (cst-matchp$ abnf::tree abnf::elem)))

Theorem: cst-matchp$-element-equiv-congruence-on-elem

(defthm cst-matchp$-element-equiv-congruence-on-elem
  (implies (abnf::element-equiv abnf::elem elem-equiv)
           (equal (cst-matchp$ abnf::tree abnf::elem)
                  (cst-matchp$ abnf::tree elem-equiv)))
  :rule-classes :congruence)