		Search-engine friendly clone of the ACL2 documentation.

Identifiers

Nonascii-identifier-start-p

Check if a non-ASCII Java Unicode character can start identifiers.

This is like ascii-identifier-start-p, but for Unicode characters that are not ASCII.

For now we leave this predicate almost completely unspecified, by introducing it as a weakly constrained function. We only require it to have a guard consisting of the non-ASCII Java Unicode characters, to return a boolean, and to fix its input to a Java Unicode character.

Defining this predicate completely may require the development of a Unicode library in ACL2 that formalizes categories and related notions.

Definitions and Theorems

Theorem: booleanp-of-nonascii-identifier-start-p

(defthm booleanp-of-nonascii-identifier-start-p
  (booleanp (nonascii-identifier-start-p char))
  :rule-classes (:type-prescription :rewrite))

Theorem: nonascii-identifier-start-p-of-unicode-fix-char

(defthm nonascii-identifier-start-p-of-unicode-fix-char
  (equal (nonascii-identifier-start-p (unicode-fix char))
         (nonascii-identifier-start-p char)))

Theorem: nonascii-identifier-start-p-unicode-equiv-congruence-on-char

(defthm nonascii-identifier-start-p-unicode-equiv-congruence-on-char
  (implies (unicode-equiv char char-equiv)
           (equal (nonascii-identifier-start-p char)
                  (nonascii-identifier-start-p char-equiv)))
  :rule-classes :congruence)