		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-simple-escape

Validate a simple escape.

Signature
(valid-simple-escape esc) → code
Arguments: esc — Guard (simple-escapep esc).
Returns: code — Type (natp code).

Simple escapes are always valid. This function returns their ASCII codes. Note that these always fit in any of the types mentioned in [C:6.4.4.4/4]. The GCC escape \% is like the character %.

Definitions and Theorems

Function: valid-simple-escape

(defun valid-simple-escape (esc)
  (declare (xargs :guard (simple-escapep esc)))
  (let ((__function__ 'valid-simple-escape))
    (declare (ignorable __function__))
    (simple-escape-case esc
                        :squote (char-code #\')
                        :dquote (char-code #\")
                        :qmark (char-code #\?)
                        :bslash (char-code #\\)
                        :a 7
                        :b 8
                        :f 12
                        :n 10
                        :r 13
                        :t 9
                        :v 11
                        :percent (char-code #\%))))

Theorem: natp-of-valid-simple-escape

(defthm natp-of-valid-simple-escape
  (b* ((code (valid-simple-escape esc)))
    (natp code))
  :rule-classes :rewrite)

Theorem: valid-simple-escape-of-simple-escape-fix-esc

(defthm valid-simple-escape-of-simple-escape-fix-esc
  (equal (valid-simple-escape (simple-escape-fix esc))
         (valid-simple-escape esc)))

Theorem: valid-simple-escape-simple-escape-equiv-congruence-on-esc

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