		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Uniescape-parse-p

Check if a list of Unicode characters can be parsed into a list of trees.

This is the case when there exists a list of unicode-input-character trees that is a valid output of the parser, as characterized by uniescape-parse-constraints-p.

This should be always the case, but it remains to be proved formally.

Note that the witness function returns the parser output.

Definitions and Theorems

Theorem: uniescape-parse-p-suff

(defthm uniescape-parse-p-suff
 (implies
   (and (abnf-tree-list-with-root-p trees "unicode-input-character")
        (uniescape-parse-constraints-p unicodes trees))
   (uniescape-parse-p unicodes)))

Theorem: booleanp-of-uniescape-parse-p

(defthm booleanp-of-uniescape-parse-p
  (b* ((yes/no (uniescape-parse-p unicodes)))
    (booleanp yes/no))
  :rule-classes :rewrite)