		Search-engine friendly clone of the ACL2 documentation.

Nrev

Nrev-push

Fundamental operation to extend nrev with a new element.

Signature: (nrev-push a nrev) → nrev'

In the logic, this sets:

nrev' := (rcons a nrev)

In the pure ACL2 implementation, the underlying representation of nrev keeps the elements in reverse order, so nrev-push takes just a single cons.

In the optimized implementation, this operation creates a cons and then destructively extends the rightmost cons cell, like a Common Lisp rplacd operation.

Definitions and Theorems

Function: nrev$a-push

(defun nrev$a-push (a nrev$a)
  (declare (xargs :guard t))
  (rcons a nrev$a))

Function: nrev$c-push

(defun nrev$c-push (a nrev$c)
  (declare (xargs :stobjs nrev$c))
  (let* ((acc (nrev$c-acc nrev$c))
         (acc (cons a acc)))
    (update-nrev$c-acc acc nrev$c)))