		Search-engine friendly clone of the ACL2 documentation.

Esim-steps

Esim-faig-steps

ESIM stepping function.

Signature
(esim-faig-steps mod ins st) → (mv * *)

Definitions and Theorems

Function: esim-faig-steps

(defun esim-faig-steps (mod ins st)
       (declare (xargs :guard t))
       (let ((__function__ 'esim-faig-steps))
            (declare (ignorable __function__))
            (b* (((when (atom ins)) (mv nil nil))
                 ((mv nst out)
                  (b* ((in (car ins)) ((with-fast in st)))
                      (esim-faig-3v mod in st)))
                 ((mv nsts outs)
                  (esim-faig-steps mod (cdr ins) nst)))
                (mv (cons nst nsts) (cons out outs)))))