		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Keyword-abnf-stringp

Check if an ABNF string (i.e. a list of natural numbers) is the fringe of a tree for a keyword.

Definitions and Theorems

Theorem: keyword-abnf-stringp-suff

(defthm keyword-abnf-stringp-suff
  (implies (and (abnf-tree-with-root-p tree "keyword")
                (equal (nat-list-fix string)
                       (abnf::tree->string tree)))
           (keyword-abnf-stringp string)))

Theorem: booleanp-of-keyword-abnf-stringp

(defthm booleanp-of-keyword-abnf-stringp
  (b* ((yes/no (keyword-abnf-stringp string)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: treep-of-keyword-abnf-stringp-witness

(defthm treep-of-keyword-abnf-stringp-witness
  (implies (keyword-abnf-stringp string)
           (abnf::treep (keyword-abnf-stringp-witness string))))

Theorem: keyword-abnf-stringp-of-nat-list-fix-string

(defthm keyword-abnf-stringp-of-nat-list-fix-string
  (equal (keyword-abnf-stringp (nat-list-fix string))
         (keyword-abnf-stringp string)))

Theorem: keyword-abnf-stringp-nat-list-equiv-congruence-on-string

(defthm keyword-abnf-stringp-nat-list-equiv-congruence-on-string
  (implies (acl2::nat-list-equiv string string-equiv)
           (equal (keyword-abnf-stringp string)
                  (keyword-abnf-stringp string-equiv)))
  :rule-classes :congruence)