		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 [C17: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)))
  (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)