		Search-engine friendly clone of the ACL2 documentation.

Keywords-grammar-validation

Grammar-jkeywordp

Definition of (non-restricted) keywords based on the grammar.

This defines a (non-restricted) keyword as a string at the leaves of a terminated tree rooted at the keyword nonterminal.

Definitions and Theorems

Theorem: grammar-jkeywordp-suff

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

Theorem: booleanp-of-grammar-jkeywordp

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