		Search-engine friendly clone of the ACL2 documentation.

Grammar

Abnf-tree-list-with-root-p

Lift abnf-tree-with-root-p to lists.

Signature
(abnf-tree-list-with-root-p x rulename) → std::bool

This is an ordinary std::deflist. It is "strict" in that it requires x to be a "properly" nil-terminated list.

Definitions and Theorems

Function: abnf-tree-list-with-root-p

(defun abnf-tree-list-with-root-p (x rulename)
  (declare (xargs :guard (stringp rulename)))
  (let ((__function__ 'abnf-tree-list-with-root-p))
    (declare (ignorable __function__))
    (if (consp x)
        (and (abnf-tree-with-root-p (car x) rulename)
             (abnf-tree-list-with-root-p (cdr x)
                                         rulename))
      (null x))))

Theorem: abnf-tree-listp-when-abnf-tree-list-with-root-p

(defthm abnf-tree-listp-when-abnf-tree-list-with-root-p
  (implies (abnf-tree-list-with-root-p trees rulename)
           (abnf::tree-listp trees)))

Subtopics

Abnf-tree-list-with-root-p-basics: Basic theorems about abnf-tree-list-with-root-p, generated by std::deflist.