		Search-engine friendly clone of the ACL2 documentation.

Exec-character-set

Ext-exec-charp

Recognize the extended execution characters.

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

These are the non-basic exec-characters.

Definitions and Theorems

Function: ext-exec-charp

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

Theorem: booleanp-of-ext-exec-charp

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

Theorem: exec-charp-alt-def

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