		Search-engine friendly clone of the ACL2 documentation.

Html-encoding

Html-encode-chars-basic-aux

Convert a character list into HTML (simple version, no column/tabsize support).

Signature
(html-encode-chars-basic-aux x acc) → new-acc
Arguments: x — The characters to convert.
Guard (character-listp x).; acc — Accumulator for output characters, reverse order.
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: html-encode-chars-basic-aux

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

Theorem: character-listp-of-html-encode-chars-basic-aux

(defthm character-listp-of-html-encode-chars-basic-aux
  (implies (character-listp acc)
           (b* ((new-acc (html-encode-chars-basic-aux x acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)

Theorem: html-encode-chars-basic-aux-of-make-character-list-x

(defthm html-encode-chars-basic-aux-of-make-character-list-x
  (equal (html-encode-chars-basic-aux (make-character-list x)
                                      acc)
         (html-encode-chars-basic-aux x acc)))

Theorem: html-encode-chars-basic-aux-charlisteqv-congruence-on-x

(defthm html-encode-chars-basic-aux-charlisteqv-congruence-on-x
  (implies (charlisteqv x x-equiv)
           (equal (html-encode-chars-basic-aux x acc)
                  (html-encode-chars-basic-aux x-equiv acc)))
  :rule-classes :congruence)