		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Uniescape-candidate-p

Check if, in a list of Unicode characters, a Unicode escape may start at position pos.

Signature
(uniescape-candidate-p pos unicodes) → yes/no
Arguments: pos — Guard (natp pos).; unicodes — Guard (unicode-listp unicodes).
Returns: yes/no — Type (booleanp yes/no).

This notion is not explicitly defined in [JLS14:3.3], but it is useful for our formalization. A candidate position for (the start of) a Unicode escape is the position of an eligible backslash followed by a non-zero number of `u' letters.

When there is such a candidate position in a list of Unicode characters, either the candidate is an actual Unicode escape, or the list of Unicode characters is invalid. This is defined subsequently.

Definitions and Theorems

Function: uniescape-candidate-p

(defun uniescape-candidate-p (pos unicodes)
  (declare (xargs :guard (and (natp pos)
                              (unicode-listp unicodes))))
  (declare (xargs :guard (< pos (len unicodes))))
  (and (eligible-backslash-p pos unicodes)
       (nonzero-uletters-after-p pos unicodes)))

Theorem: booleanp-of-uniescape-candidate-p

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