		Search-engine friendly clone of the ACL2 documentation.

Grammar-new

Abnf-tree-with-root-p

Recognize terminated ABNF trees rooted at rulename, for the ABNF grammar of Yul.

Signature
(abnf-tree-with-root-p tree rulename) → yes/no
Arguments: rulename — Guard (stringp rulename).
Returns: yes/no — Type (booleanp yes/no).

The tree has ASCII codes at its leaves.

Definitions and Theorems

Function: abnf-tree-with-root-p

(defun abnf-tree-with-root-p (tree rulename)
  (declare (xargs :guard (stringp rulename)))
  (and (abnf::treep tree)
       (abnf::tree-terminatedp tree)
       (abnf::tree-match-element-p
            tree
            (abnf::element-rulename (abnf::rulename rulename))
            *grammar-new*)))

Theorem: booleanp-of-abnf-tree-with-root-p

(defthm booleanp-of-abnf-tree-with-root-p
  (b* ((yes/no (abnf-tree-with-root-p tree rulename)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: abnf-treep-when-abnf-tree-with-root-p

(defthm abnf-treep-when-abnf-tree-with-root-p
  (implies (abnf-tree-with-root-p tree rulename)
           (abnf::treep tree)))

Theorem: not-abnf-tree-with-root-p-of-nil

(defthm not-abnf-tree-with-root-p-of-nil
  (not (abnf-tree-with-root-p nil rulename)))

Theorem: abnf-tree-with-root-p-of-str-fix-rulename

(defthm abnf-tree-with-root-p-of-str-fix-rulename
  (equal (abnf-tree-with-root-p tree (acl2::str-fix rulename))
         (abnf-tree-with-root-p tree rulename)))

Theorem: abnf-tree-with-root-p-streqv-congruence-on-rulename

(defthm abnf-tree-with-root-p-streqv-congruence-on-rulename
  (implies (acl2::streqv rulename rulename-equiv)
           (equal (abnf-tree-with-root-p tree rulename)
                  (abnf-tree-with-root-p tree rulename-equiv)))
  :rule-classes :congruence)