		Search-engine friendly clone of the ACL2 documentation.

Grammar-parser-disambiguating-restrictions

Tree-rulelist-restriction-p

Restrictions on the rulelist trees generated by the parser.

Signature
(tree-rulelist-restriction-p tree) → yes/no
Arguments: tree — Guard (treep tree).
Returns: yes/no — Type (booleanp yes/no).

This lifts the restriction captured by tree-list-*-rule-/-*cwsp-cnl-restriction-p from *( rule / (*c-wsp c-nl) ) to rulelist. The restriction only applies to the subtrees after the first one.

Definitions and Theorems

Function: tree-rulelist-restriction-p

(defun tree-rulelist-restriction-p (tree)
 (declare (xargs :guard (treep tree)))
 (declare
  (xargs
       :guard
       (and (tree-match-element-p tree (element-rulename *rulelist*)
                                  *grammar*)
            (tree-terminatedp tree))))
 (b* ((subtrees (car (tree-nonleaf->branches tree))))
  (or (not (consp subtrees))
      (tree-list-*-rule-/-*cwsp-cnl-restriction-p (cdr subtrees)))))

Theorem: booleanp-of-tree-rulelist-restriction-p

(defthm booleanp-of-tree-rulelist-restriction-p
  (b* ((yes/no (tree-rulelist-restriction-p tree)))
    (booleanp yes/no))
  :rule-classes :rewrite)