		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-standardp

Simple-escape-standardp

Signature
(simple-escape-standardp simple-escape) → fty::result
Arguments: simple-escape — Guard (simple-escapep simple-escape).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: simple-escape-standardp

(defun simple-escape-standardp (simple-escape)
  (declare (xargs :guard (simple-escapep simple-escape)))
  (declare (ignorable simple-escape))
  (let ((__function__ 'simple-escape-standardp))
    (declare (ignorable __function__))
    (simple-escape-case simple-escape
                        :squote t
                        :dquote t
                        :qmark t
                        :bslash t
                        :a t
                        :b t
                        :f t
                        :n t
                        :r t
                        :t t
                        :v t
                        :percent nil)))

Theorem: booleanp-of-simple-escape-standardp

(defthm booleanp-of-simple-escape-standardp
  (b* ((fty::result (simple-escape-standardp simple-escape)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: simple-escape-standardp-of-simple-escape-fix-simple-escape

(defthm simple-escape-standardp-of-simple-escape-fix-simple-escape
  (equal (simple-escape-standardp (simple-escape-fix simple-escape))
         (simple-escape-standardp simple-escape)))

Theorem: simple-escape-standardp-simple-escape-equiv-congruence-on-simple-escape

(defthm
 simple-escape-standardp-simple-escape-equiv-congruence-on-simple-escape
 (implies (simple-escape-equiv simple-escape simple-escape-equiv)
          (equal (simple-escape-standardp simple-escape)
                 (simple-escape-standardp simple-escape-equiv)))
 :rule-classes :congruence)