		Search-engine friendly clone of the ACL2 documentation.

Source-character-set

Ext-source-charp

Recognize the extended source characters.

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

These are the non-basic source-characters.

Definitions and Theorems

Function: ext-source-charp

(defun ext-source-charp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'ext-source-charp))
    (declare (ignorable __function__))
    (and (source-charp x)
         (not (basic-source-charp x)))))

Theorem: booleanp-of-ext-source-charp

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

Theorem: source-charp-alt-def

(defthm source-charp-alt-def
  (equal (source-charp x)
         (or (basic-source-charp x)
             (ext-source-charp x))))