		Search-engine friendly clone of the ACL2 documentation.

Parser

Token-rootp

Check if the given token has the given rule name as root.

Signature
(token-rootp rulename token) → yes/no
Arguments: rulename — Guard (stringp rulename).; token — Guard (abnf::tree-optionp token).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: token-rootp

(defun token-rootp (rulename token)
  (declare (xargs :guard (and (stringp rulename)
                              (abnf::tree-optionp token))))
  (let ((__function__ 'token-rootp))
    (declare (ignorable __function__))
    (abnf-tree-with-root-p (abnf::tree-option-fix token)
                           rulename)))

Theorem: booleanp-of-token-rootp

(defthm booleanp-of-token-rootp
  (b* ((yes/no (token-rootp rulename token)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: token-nonnil-when-rootp

(defthm token-nonnil-when-rootp
  (implies (token-rootp string token)
           token)
  :rule-classes :forward-chaining)

Theorem: token-rootp-of-str-fix-rulename

(defthm token-rootp-of-str-fix-rulename
  (equal (token-rootp (str-fix rulename) token)
         (token-rootp rulename token)))

Theorem: token-rootp-streqv-congruence-on-rulename

(defthm token-rootp-streqv-congruence-on-rulename
  (implies (acl2::streqv rulename rulename-equiv)
           (equal (token-rootp rulename token)
                  (token-rootp rulename-equiv token)))
  :rule-classes :congruence)

Theorem: token-rootp-of-tree-option-fix-token

(defthm token-rootp-of-tree-option-fix-token
  (equal (token-rootp rulename (abnf::tree-option-fix token))
         (token-rootp rulename token)))

Theorem: token-rootp-tree-option-equiv-congruence-on-token

(defthm token-rootp-tree-option-equiv-congruence-on-token
  (implies (abnf::tree-option-equiv token token-equiv)
           (equal (token-rootp rulename token)
                  (token-rootp rulename token-equiv)))
  :rule-classes :congruence)