(stv2c-ins-structfields ins stv acc) → new-acc
Function:
(defun stv2c-ins-structfields (ins stv acc) (declare (xargs :guard (processed-stv-p stv))) (let ((__function__ 'stv2c-ins-structfields)) (declare (ignorable __function__)) (b* (((when (atom ins)) acc) ((unless (symbolp (car ins))) (raise "STV input not a symbol? ~x0" (car ins)) acc) (c-name (stv2c-c-symbol-name (car ins))) (width (stv-in->width (car ins) stv)) (acc (str::revappend-chars " fourval<" acc)) (acc (str::revappend-chars (str::natstr width) acc)) (acc (str::revappend-chars "> " acc)) (acc (str::revappend-chars c-name acc)) (acc (str::revappend-chars ";" acc)) (acc (cons #\Newline acc))) (stv2c-ins-structfields (cdr ins) stv acc))))
Theorem:
(defthm character-listp-of-stv2c-ins-structfields (implies (character-listp acc) (b* ((new-acc (stv2c-ins-structfields ins stv acc))) (character-listp new-acc))) :rule-classes :rewrite)