		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Symbol-abnf-stringp

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

Definitions and Theorems

Theorem: symbol-abnf-stringp-suff

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

Theorem: booleanp-of-symbol-abnf-stringp

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

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

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

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

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

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

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