		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-standardp

S-char-standardp

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

Definitions and Theorems

Function: s-char-standardp

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

Theorem: booleanp-of-s-char-standardp

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

Theorem: s-char-standardp-of-s-char-fix-s-char

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

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

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