		Search-engine friendly clone of the ACL2 documentation.

Unicode-escapes

Even-backslashes-before-p

Check if, in a list of Unicode characters, the character at position pos is preceded by an even number of backslashes.

This is used to define the notion of eligible backslash.

Note that (take n (nthcdr (- pos n) unicodes)) consists of the characters from position (- pos n) to (- pos 1), both extremes inclusive (positions in lists are zero-based).

Formally, it is not sufficient just to say that there are n backslashes just before pos with n even: we must also say that there is no backslash just before (- pos n), either because the list starts there (i.e. pos is n) or because the character at (- (- pos n) 1) is not a backslash; this is expressed by the last conjunct inside the quantification.

This definition works fine if n is 0.

Definitions and Theorems

Theorem: even-backslashes-before-p-suff

(defthm even-backslashes-before-p-suff
  (implies (and (natp n)
                (evenp n)
                (>= (- pos n) 0)
                (equal (take n (nthcdr (- pos n) unicodes))
                       (repeat n (char-code #\\)))
                (or (equal (- pos n) 0)
                    (not (equal (nth (1- (- pos n)) unicodes)
                                (char-code #\\)))))
           (even-backslashes-before-p pos unicodes)))

Theorem: booleanp-of-even-backslashes-before-p

(defthm booleanp-of-even-backslashes-before-p
  (b* ((yes/no (even-backslashes-before-p pos unicodes)))
    (booleanp yes/no))
  :rule-classes :rewrite)