		Search-engine friendly clone of the ACL2 documentation.

Abnf-tree-utilities

Check-tree-nonleaf?

Check if an ABNF tree is a non-leaf tree, returning its rule name (or nil if absent) if successful.

Signature
(check-tree-nonleaf? tree) → rulename?
Arguments: tree — Guard (abnf::treep tree).
Returns: rulename? — Type (maybe-string-resultp rulename?).

Definitions and Theorems

Function: check-tree-nonleaf?

(defun check-tree-nonleaf? (tree)
  (declare (xargs :guard (abnf::treep tree)))
  (let ((__function__ 'check-tree-nonleaf?))
    (declare (ignorable __function__))
    (if (abnf::tree-case tree :nonleaf)
        (b* ((rulename? (abnf::tree-nonleaf->rulename? tree)))
          (if rulename? (abnf::rulename->get rulename?)
            nil))
      (reserrf (list :required :nonleaf
                     :found (tree-info-for-error tree))))))

Theorem: maybe-string-resultp-of-check-tree-nonleaf?

(defthm maybe-string-resultp-of-check-tree-nonleaf?
  (b* ((rulename? (check-tree-nonleaf? tree)))
    (maybe-string-resultp rulename?))
  :rule-classes :rewrite)

Theorem: check-tree-nonleaf?-of-tree-fix-tree

(defthm check-tree-nonleaf?-of-tree-fix-tree
  (equal (check-tree-nonleaf? (abnf::tree-fix tree))
         (check-tree-nonleaf? tree)))

Theorem: check-tree-nonleaf?-tree-equiv-congruence-on-tree

(defthm check-tree-nonleaf?-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (check-tree-nonleaf? tree)
                  (check-tree-nonleaf? tree-equiv)))
  :rule-classes :congruence)