		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-standardp

C-char-standardp

Signature
(c-char-standardp c-char) → fty::result
Arguments: c-char — Guard (c-char-p c-char).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: c-char-standardp

(defun c-char-standardp (c-char)
 (declare (xargs :guard (c-char-p c-char)))
 (declare (ignorable c-char))
 (let ((__function__ 'c-char-standardp))
   (declare (ignorable __function__))
   (c-char-case
        c-char
        :char t
        :escape (escape-standardp (c-char-escape->escape c-char)))))

Theorem: booleanp-of-c-char-standardp

(defthm booleanp-of-c-char-standardp
  (b* ((fty::result (c-char-standardp c-char)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: c-char-standardp-of-c-char-fix-c-char

(defthm c-char-standardp-of-c-char-fix-c-char
  (equal (c-char-standardp (c-char-fix c-char))
         (c-char-standardp c-char)))

Theorem: c-char-standardp-c-char-equiv-congruence-on-c-char

(defthm c-char-standardp-c-char-equiv-congruence-on-c-char
  (implies (c-char-equiv c-char c-char-equiv)
           (equal (c-char-standardp c-char)
                  (c-char-standardp c-char-equiv)))
  :rule-classes :congruence)