		Search-engine friendly clone of the ACL2 documentation.

Character-literals

Unicode-charlit-char-p

Recognizer for unicode-charlit-char.

Signature
(unicode-charlit-char-p x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: unicode-charlit-char-p

(defun unicode-charlit-char-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'unicode-charlit-char-p))
    (declare (ignorable __function__))
    (and (unicode-input-char-p x)
         (not (member (unicode-input-char->unicode x)
                      (list (char-code #\Return)
                            (char-code #\Newline)
                            (char-code #\')
                            (char-code #\\)))))))

Theorem: booleanp-of-unicode-charlit-char-p

(defthm booleanp-of-unicode-charlit-char-p
  (b* ((yes/no (unicode-charlit-char-p x)))
    (booleanp yes/no))
  :rule-classes :rewrite)