		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)))
  (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-list-with-root-p-of-str-fix-rulename

(defthm abnf-tree-list-with-root-p-of-str-fix-rulename
  (equal (abnf-tree-list-with-root-p x (str-fix rulename))
         (abnf-tree-list-with-root-p x rulename)))

Theorem: abnf-tree-list-with-root-p-streqv-congruence-on-rulename

(defthm abnf-tree-list-with-root-p-streqv-congruence-on-rulename
  (implies (acl2::streqv rulename rulename-equiv)
           (equal (abnf-tree-list-with-root-p x rulename)
                  (abnf-tree-list-with-root-p x rulename-equiv)))
  :rule-classes :congruence)

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)))

Theorem: unicode-listp-of-string-of-abnf-tree-list-with-root

(defthm unicode-listp-of-string-of-abnf-tree-list-with-root
  (implies (abnf-tree-list-with-root-p trees rulename)
           (unicode-listp (abnf::tree-list->string trees))))

Subtopics

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