		Search-engine friendly clone of the ACL2 documentation.

Esim-steps

Esim-sexpr-steps

ESIM stepping function.

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

Definitions and Theorems

Function: esim-sexpr-steps

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