		Search-engine friendly clone of the ACL2 documentation.

Keywords-grammar-validation

Grammar-reserved-keywordp

Definition of reserved keywords based on the grammar.

This defines a reserved keyword as a string at the leaves of a terminated tree rooted at the reserved-keyword nonterminal.

Definitions and Theorems

Theorem: grammar-reserved-keywordp-suff

(defthm grammar-reserved-keywordp-suff
  (implies (and (abnf-tree-with-root-p tree "reserved-keyword")
                (equal (abnf::tree->string tree) x))
           (grammar-reserved-keywordp x)))

Theorem: booleanp-of-grammar-reserved-keywordp

(defthm booleanp-of-grammar-reserved-keywordp
  (b* ((yes/no (grammar-reserved-keywordp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)