		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Uniescapep

Check if, in a list of Unicode characters, there is a Unicode escape at position pos.

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

This is true when there is a valid Unicode escape at pos, i.e. if there is an eligible backslah at pos followed by one or more `u' letters that are followed by four hexadecimal digits.

Definitions and Theorems

Function: uniescapep

(defun uniescapep (pos unicodes)
  (declare (xargs :guard (and (natp pos)
                              (unicode-listp unicodes))))
  (declare (xargs :guard (< pos (len unicodes))))
  (and (uniescape-candidate-p pos unicodes)
       (uniescape-candidate-valid-p pos unicodes)))

Theorem: booleanp-of-uniescapep

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