		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Some-uniescape-candidate-invalid-p

Check if a list of Unicode characters includes an invalid Unicode escape candidate.

This is used to formalize when the list of Unicode characters does not satisfy the constraints related to Unicode escapes, i.e. the whole sequence of Unicode characters is not a valid Java program right at the first lexical translation step.

This is the case when there is at least one candidate Unicode escape that is invalid. That is, there is an eligible backslash followed by one or more `u' letters that are not followed by four hexadecimal digits.

Definitions and Theorems

Theorem: some-uniescape-candidate-invalid-p-suff

(defthm some-uniescape-candidate-invalid-p-suff
  (implies (and (integer-range-p 0 (len unicodes) pos)
                (uniescape-candidate-p pos unicodes)
                (not (uniescape-candidate-valid-p pos unicodes)))
           (some-uniescape-candidate-invalid-p unicodes)))

Theorem: booleanp-of-some-uniescape-candidate-invalid-p

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