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