		Search-engine friendly clone of the ACL2 documentation.

Nrev-demo

Map-tr

Conventional tail-recursive core for mapping f.

Signature
(map-tr x acc) → *

This returns the elements in backwards order.

Definitions and Theorems

Function: map-tr

(defun map-tr (x acc)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'map-tr))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        acc
      (map-tr (cdr x)
              (cons (f (car x)) acc)))))

Theorem: map-tr-correct

(defthm map-tr-correct
  (equal (map-tr x acc)
         (revappend (map-spec x) acc)))