		Search-engine friendly clone of the ACL2 documentation.

Nrev-demo

Map-impl

nrev-based tail-recursive core for mapping f.

Signature
(map-impl x nrev) → nrev

This is essentially similar to map-tr.

The most interesting part of this is the correctness theorem:

Thanks to abstract stobjs, we can just write our theorem as if nrev is an ordinary list.
Thanks to the rcons-based logical story for nrev, our theorem doesn't have to be in terms of revappend as it does in map-tr. Instead, we can just use ordinary append.

Definitions and Theorems

Function: map-impl

(defun map-impl (x nrev)
  (declare (xargs :stobjs (nrev)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'map-impl))
    (declare (ignorable acl2::__function__))
    (b* (((when (atom x)) (nrev-fix nrev))
         (nrev (nrev-push (f (car x)) nrev)))
      (map-impl (cdr x) nrev))))

Theorem: map-impl-correct

(defthm map-impl-correct
  (equal (map-impl x nrev)
         (append nrev (map-spec x))))