		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Eligible-backslash-p

Check if, in a list of Unicode characters, the character at position pos is an eligible backslash.

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

This is the case when the character at pos is a backslash and is preceded by an even number of backslashes.

Definitions and Theorems

Function: eligible-backslash-p

(defun eligible-backslash-p (pos unicodes)
  (declare (xargs :guard (and (natp pos)
                              (unicode-listp unicodes))))
  (declare (xargs :guard (< pos (len unicodes))))
  (and (equal (nth pos unicodes)
              (char-code #\\))
       (even-backslashes-before-p pos unicodes)))

Theorem: booleanp-of-eligible-backslash-p

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