		Search-engine friendly clone of the ACL2 documentation.

Parser

Cst2ast-xhh

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

Definitions and Theorems

Function: cst2ast-xhh

(defun cst2ast-xhh (escape-contents)
 (declare (xargs :guard (abnf::tree-listp escape-contents)))
 (let ((__function__ 'cst2ast-xhh))
  (declare (ignorable __function__))
  (b*
   (((unless (and (abnf::tree-listp escape-contents)
                  (equal (len escape-contents) 2)))
     (reserrf "unexpected input to cst2ast-xhh"))
    (fringe (abnf::tree-list->string escape-contents))
    ((unless (and (equal (len fringe) 2)
                  (acl2::unsigned-byte-listp 8 fringe)))
     (reserrf "unexpected input to cst2ast-xhh 2"))
    (hex-digit-chars (acl2::nats=>chars fringe))
    ((unless (and (str::hex-digit-char-list*p hex-digit-chars)
                  (str::hex-digit-char-p (first hex-digit-chars))
                  (str::hex-digit-char-p (second hex-digit-chars))))
     (reserrf "unexpected input to cst2ast-xhh 3")))
   (make-escape-x
       :get
       (make-hex-pair
            :1st (make-hex-digit :get (first hex-digit-chars))
            :2nd (make-hex-digit :get (second hex-digit-chars)))))))

Theorem: escape-resultp-of-cst2ast-xhh

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