		Search-engine friendly clone of the ACL2 documentation.

Stv2c-outs-structdef

Stv2c-outs-structfields

Signature
(stv2c-outs-structfields outs stv acc) → new-acc
Arguments: outs — Initially the stv->outs 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-outs-structfields

(defun stv2c-outs-structfields (outs stv acc)
  (declare (xargs :guard (processed-stv-p stv)))
  (let ((__function__ 'stv2c-outs-structfields))
    (declare (ignorable __function__))
    (b* (((when (atom outs)) acc)
         ((unless (symbolp (car outs)))
          (raise "STV output not a symbol? ~x0"
                 (car outs))
          acc)
         (c-name (stv2c-c-symbol-name (car outs)))
         (width (stv-out->width (car outs) 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-outs-structfields (cdr outs)
                               stv acc))))

Theorem: character-listp-of-stv2c-outs-structfields

(defthm character-listp-of-stv2c-outs-structfields
  (implies (character-listp acc)
           (b* ((new-acc (stv2c-outs-structfields outs stv acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)