		Search-engine friendly clone of the ACL2 documentation.

Json-encoding

Json-encode-chars

Signature
(json-encode-chars x acc) → new-acc
Arguments: x — Guard (character-listp x).
Returns: new-acc — Type (character-listp new-acc), given (and (character-listp x) (character-listp acc)).

Definitions and Theorems

Function: json-encode-chars

(defun json-encode-chars (x acc)
  (declare (xargs :guard (character-listp x)))
  (let ((__function__ 'json-encode-chars))
    (declare (ignorable __function__))
    (b* (((when (atom x)) acc)
         (acc (json-encode-char (car x) acc)))
      (json-encode-chars (cdr x) acc))))

Theorem: character-listp-of-json-encode-chars

(defthm character-listp-of-json-encode-chars
  (implies (and (character-listp x)
                (character-listp acc))
           (b* ((new-acc (json-encode-chars x acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)