		Search-engine friendly clone of the ACL2 documentation.

Eval-pre-map

Signature
(eval-pre-map x state) → (mv * * state)

Definitions and Theorems

Function: eval-pre-map

(defun eval-pre-map (x state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'eval-pre-map))
    (declare (ignorable __function__))
    (if (atom x)
        (mv nil x state)
      (b* (((mv ?erp val state)
            (trans-eval (car x)
                        'eval-pre-map
                        state t))
           ((mv erp rest state)
            (eval-pre-map (cdr x) state))
           (all (cons (cdr val) rest))
           (erp (or erp (if (inst-list-p all) nil t))))
        (mv erp all state)))))