|
|
|---|
|
|
|
|---|
Definition of contextual keywords based on the grammar.
This defines a contextual keyword as a string at the leaves of
a terminated tree rooted at the
Theorem:
(defthm grammar-contextual-keywordp-suff (implies (and (abnf-tree-with-root-p tree "contextual-keyword") (equal (abnf::tree->string tree) x)) (grammar-contextual-keywordp x)))
Theorem:
(defthm booleanp-of-grammar-contextual-keywordp (b* ((yes/no (grammar-contextual-keywordp x))) (booleanp yes/no)) :rule-classes :rewrite)