		Search-engine friendly clone of the ACL2 documentation.

Source-character-set

Ascii-basic-source-charp

Recognize the ACL2 ASCII characters that correspond to the members of the basic source character set in C.

Signature
(ascii-basic-source-charp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

These are uppercase and lowercase letters, decimal digits, graphic characters, space, horizontal tab, vertical tab, and form feed [C:5.2.1/3].

Note that the double quote character and the backslash character must be escaped (i.e. preceded by a backslash) in ACL2 strings. The ACL2 character #\Space has ASCII code 32 and corresponds to space. The ACL2 character #\Tab has ASCII code 9 and corresponds to horizontal tab. The ACL2 character with ASCII code 11 corresponds to vertical tab. The ACL2 character #\Page has ASCII code 12 and corresponds to form feed.

Definitions and Theorems

Function: ascii-basic-source-charp

(defun ascii-basic-source-charp (x)
  (declare (xargs :guard t))
  (or (and (common-lisp::member
                x
                (acl2::explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ"))
           t)
      (and (common-lisp::member
                x
                (acl2::explode "abcdefghijklmnopqrstuvwxyz"))
           t)
      (and (common-lisp::member x (acl2::explode "0123456789"))
           t)
      (and (common-lisp::member
                x
                (acl2::explode "!\"#%&'()*+,-./:;<=>?[\\]^_{|}~"))
           t)
      (and (common-lisp::member x
                                (list #\Space #\Tab (code-char 11)
                                      #\Page))
           t)))

Theorem: booleanp-of-ascii-basic-source-charp

(defthm booleanp-of-ascii-basic-source-charp
  (b* ((yes/no (ascii-basic-source-charp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: characterp-when-ascii-basic-source-charp

(defthm characterp-when-ascii-basic-source-charp
  (implies (ascii-basic-source-charp x)
           (characterp x))
  :rule-classes :compound-recognizer)