		Search-engine friendly clone of the ACL2 documentation.

Nrev-demo

My-map

nrev-based mbe of map-spec and map-impl.

Signature
(my-map x) → *

This is a bit more involved than map-traditional because we need to use with-local-stobj to create our temporary accumulator, run our implementation, and then extract the results with nrev-finish. Fortunately that can all be wrapped up into with-local-nrev.

Definitions and Theorems

Function: my-map

(defun my-map (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'my-map))
    (declare (ignorable acl2::__function__))
    (mbe :logic (map-spec x)
         :exec (with-local-nrev (map-impl x nrev)))))