		Search-engine friendly clone of the ACL2 documentation.

Esim-steps

Esim-sexpr-simp-new-probe-steps

ESIM stepping function.

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

Definitions and Theorems

Function: esim-sexpr-simp-new-probe-steps

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