		Search-engine friendly clone of the ACL2 documentation.

Stv2c-outs-structdef

Stv2c-outs-structname

Signature
(stv2c-outs-structname stv) → *
Arguments: stv — Guard (processed-stv-p stv).

Definitions and Theorems

Function: stv2c-outs-structname

(defun stv2c-outs-structname (stv)
  (declare (xargs :guard (processed-stv-p stv)))
  (let ((__function__ 'stv2c-outs-structname))
    (declare (ignorable __function__))
    (b* (((processed-stv stv) stv)
         (c-name (stv2c-c-symbol-name stv.name)))
      (str::cat c-name "_outs"))))