		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)