		Search-engine friendly clone of the ACL2 documentation.

Exec-character-set

Ascii-basic-exec-charp

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

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

These are the ones for the basic source character set, plus null character, alert, backspace, carriage return, and new line [C17:5.2.1/2-3].

The ACL2 character with ASCII code 0 corresponds to the null character. The ACL2 character with ASCII code 7 corresponds to alert. The ACL2 character with ASCII code 8 corresponds to backspace. The ACL2 charater #\Return has ASCII code 13 and corresponds to carriage return. The ACL2 character #\Newline has ASCII code 10 and corresponds to new line.

Definitions and Theorems

Function: ascii-basic-exec-charp

(defun ascii-basic-exec-charp (x)
  (declare (xargs :guard t))
  (or (ascii-basic-source-charp x)
      (and (common-lisp::member x
                                (list (code-char 0)
                                      (code-char 7)
                                      (code-char 8)
                                      #\Return #\Newline))
           t)))

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

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

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

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