Convert a vl-bitlist into the corresponding string, e.g.,
(vl-bitlist->string x) → str
Function:
(defun vl-bitlist->string (x) (declare (xargs :guard (vl-bitlist-p x))) (let ((__function__ 'vl-bitlist->string)) (declare (ignorable __function__)) (implode (vl-bitlist->charlist x))))
Theorem:
(defthm stringp-of-vl-bitlist->string (b* ((str (vl-bitlist->string x))) (stringp str)) :rule-classes :type-prescription)
Theorem:
(defthm vl-bitlist->string-of-vl-bitlist-fix-x (equal (vl-bitlist->string (vl-bitlist-fix x)) (vl-bitlist->string x)))
Theorem:
(defthm vl-bitlist->string-vl-bitlist-equiv-congruence-on-x (implies (vl-bitlist-equiv x x-equiv) (equal (vl-bitlist->string x) (vl-bitlist->string x-equiv))) :rule-classes :congruence)