		Search-engine friendly clone of the ACL2 documentation.

Tokenizer

Is-tree-rulename?

True if tree is nonleaf for rule rulename-string.

Signature
(is-tree-rulename? tree rulename-string) → yes/no
Arguments: tree — Guard (abnf::treep tree).; rulename-string — Guard (stringp rulename-string).
Returns: yes/no — Type (booleanp yes/no).

Does not details of the internal structure.

Definitions and Theorems

Function: is-tree-rulename?

(defun is-tree-rulename? (tree rulename-string)
  (declare (xargs :guard (and (abnf::treep tree)
                              (stringp rulename-string))))
  (let ((__function__ 'is-tree-rulename?))
    (declare (ignorable __function__))
    (and (abnf::treep tree)
         (abnf::tree-case tree :nonleaf)
         (equal (abnf::tree-nonleaf->rulename? tree)
                (abnf::rulename rulename-string)))))

Theorem: booleanp-of-is-tree-rulename?

(defthm booleanp-of-is-tree-rulename?
  (b* ((yes/no (is-tree-rulename? tree rulename-string)))
    (booleanp yes/no))
  :rule-classes :rewrite)