		Search-engine friendly clone of the ACL2 documentation.

Abnf-tree-utilities

Check-tree-leafterm

Check if an ABNF tree is a leaf tree, returning its list of natural numbers if sucessful.

Signature
(check-tree-leafterm tree) → nats
Arguments: tree — Guard (abnf::treep tree).
Returns: nats — Type (nat-list-resultp nats).

Definitions and Theorems

Function: check-tree-leafterm

(defun check-tree-leafterm (tree)
  (declare (xargs :guard (abnf::treep tree)))
  (let ((__function__ 'check-tree-leafterm))
    (declare (ignorable __function__))
    (if (abnf::tree-case tree :leafterm)
        (abnf::tree-leafterm->get tree)
      (reserrf (list :required :leafterm
                     :found (tree-info-for-error tree))))))

Theorem: nat-list-resultp-of-check-tree-leafterm

(defthm nat-list-resultp-of-check-tree-leafterm
  (b* ((nats (check-tree-leafterm tree)))
    (nat-list-resultp nats))
  :rule-classes :rewrite)

Theorem: check-tree-leafterm-of-tree-fix-tree

(defthm check-tree-leafterm-of-tree-fix-tree
  (equal (check-tree-leafterm (abnf::tree-fix tree))
         (check-tree-leafterm tree)))

Theorem: check-tree-leafterm-tree-equiv-congruence-on-tree

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