Print an HTML-encoded character-list.
(vl-html-encode-chars-aux x col tabsize acc) → (mv new-col new-acc)
Function:
(defun vl-html-encode-chars-aux (x col tabsize acc) (declare (xargs :guard (and (character-listp x) (natp col) (posp tabsize)))) (let ((__function__ 'vl-html-encode-chars-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (lnfix col) acc)) (char1 (mbe :logic (char-fix (car x)) :exec (car x))) (acc (vl-html-encode-push char1 col tabsize acc)) (col (vl-html-encode-next-col char1 col tabsize))) (vl-html-encode-chars-aux (cdr x) col tabsize acc))))
Theorem:
(defthm natp-of-vl-html-encode-chars-aux.new-col (b* (((mv ?new-col ?new-acc) (vl-html-encode-chars-aux x col tabsize acc))) (natp new-col)) :rule-classes :type-prescription)
Theorem:
(defthm character-listp-of-vl-html-encode-chars-aux.new-acc (implies (character-listp acc) (b* (((mv ?new-col ?new-acc) (vl-html-encode-chars-aux x col tabsize acc))) (character-listp new-acc))) :rule-classes :rewrite)
Theorem:
(defthm vl-html-encode-chars-aux-of-make-character-list-x (equal (vl-html-encode-chars-aux (make-character-list x) col tabsize acc) (vl-html-encode-chars-aux x col tabsize acc)))
Theorem:
(defthm vl-html-encode-chars-aux-charlisteqv-congruence-on-x (implies (str::charlisteqv x x-equiv) (equal (vl-html-encode-chars-aux x col tabsize acc) (vl-html-encode-chars-aux x-equiv col tabsize acc))) :rule-classes :congruence)
Theorem:
(defthm vl-html-encode-chars-aux-of-nfix-col (equal (vl-html-encode-chars-aux x (nfix col) tabsize acc) (vl-html-encode-chars-aux x col tabsize acc)))
Theorem:
(defthm vl-html-encode-chars-aux-nat-equiv-congruence-on-col (implies (acl2::nat-equiv col col-equiv) (equal (vl-html-encode-chars-aux x col tabsize acc) (vl-html-encode-chars-aux x col-equiv tabsize acc))) :rule-classes :congruence)
Theorem:
(defthm vl-html-encode-chars-aux-of-pos-fix-tabsize (equal (vl-html-encode-chars-aux x col (pos-fix tabsize) acc) (vl-html-encode-chars-aux x col tabsize acc)))
Theorem:
(defthm vl-html-encode-chars-aux-pos-equiv-congruence-on-tabsize (implies (acl2::pos-equiv tabsize tabsize-equiv) (equal (vl-html-encode-chars-aux x col tabsize acc) (vl-html-encode-chars-aux x col tabsize-equiv acc))) :rule-classes :congruence)