		Search-engine friendly clone of the ACL2 documentation.

Stv2c-ins-structdef

Stv2c-ins-structfields

Signature
(stv2c-ins-structfields ins stv acc) → new-acc
Arguments: ins — Initially the stv->ins from the stv.; stv — Guard (processed-stv-p stv).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: stv2c-ins-structfields

(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: character-listp-of-stv2c-ins-structfields

(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)