		Search-engine friendly clone of the ACL2 documentation.

Parser

Cst2ast-single-char

Signature
(cst2ast-single-char escape-contents) → escape
Arguments: escape-contents — Guard (abnf::tree-listp escape-contents).
Returns: escape — Type (escape-resultp escape).

Definitions and Theorems

Function: cst2ast-single-char

(defun cst2ast-single-char (escape-contents)
 (declare (xargs :guard (abnf::tree-listp escape-contents)))
 (let ((__function__ 'cst2ast-single-char))
  (declare (ignorable __function__))
  (b* (((unless (and (abnf::tree-listp escape-contents)
                     (equal (len escape-contents) 1)))
        (reserrf "unexpected input to cst2ast-single-char"))
       (fringe (abnf::tree-list->string escape-contents))
       ((unless (and (equal (len fringe) 1)
                     (acl2::unsigned-byte-listp 8 fringe)))
        (reserrf "unexpected input to cst2ast-single-char 2")))
   (case (car fringe)
    (39 (make-escape-single-quote))
    (34 (make-escape-double-quote))
    (92 (make-escape-backslash))
    (110 (make-escape-letter-n))
    (114 (make-escape-letter-r))
    (116 (make-escape-letter-t))
    (110 (make-escape-line-feed))
    (114 (make-escape-carriage-return))
    (t
     (reserrf
       "unrecognized escaped character in cst2ast-single-char"))))))

Theorem: escape-resultp-of-cst2ast-single-char

(defthm escape-resultp-of-cst2ast-single-char
  (b* ((escape (cst2ast-single-char escape-contents)))
    (escape-resultp escape))
  :rule-classes :rewrite)