		Search-engine friendly clone of the ACL2 documentation.

Stv2c-header

Stv2c-run-fnname

Signature
(stv2c-run-fnname stv) → *
Arguments: stv — Guard (processed-stv-p stv).

Definitions and Theorems

Function: stv2c-run-fnname

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