		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Identifier-abnf-stringp

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

Definitions and Theorems

Theorem: identifier-abnf-stringp-suff

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

Theorem: booleanp-of-identifier-abnf-stringp

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

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

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

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

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

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

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