Simple way to URL encode a list of characters.
(vl-url-encode-chars x) → encoded
Function:
(defun vl-url-encode-chars$inline (x) (declare (xargs :guard (character-listp x))) (let ((__function__ 'vl-url-encode-chars)) (declare (ignorable __function__)) (reverse (vl-url-encode-chars-aux x nil))))
Theorem:
(defthm character-listp-of-vl-url-encode-chars (b* ((encoded (vl-url-encode-chars$inline x))) (character-listp encoded)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-url-encode-chars (true-listp (vl-url-encode-chars x)) :rule-classes :type-prescription)
Theorem:
(defthm vl-url-encode-chars$inline-of-make-character-list-x (equal (vl-url-encode-chars$inline (make-character-list x)) (vl-url-encode-chars$inline x)))
Theorem:
(defthm vl-url-encode-chars$inline-charlisteqv-congruence-on-x (implies (str::charlisteqv x x-equiv) (equal (vl-url-encode-chars$inline x) (vl-url-encode-chars$inline x-equiv))) :rule-classes :congruence)