		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm

Svtv-to-fsm-thm-fn

Signature
(svtv-to-fsm-thm-fn thmname args state) → *

Definitions and Theorems

Function: svtv-to-fsm-thm-fn

(defun svtv-to-fsm-thm-fn (thmname args state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'svtv-to-fsm-thm-fn))
    (declare (ignorable __function__))
    (b* ((x (parse-svtv-to-fsm-thm thmname args state)))
      (list 'progn
            (svtv-to-fsm-first-thm x)
            (svtv-to-fsm-final-thm x)))))