|
|
|---|
|
|
|
|---|
Slow operation to copy the current contents of
Signature:
This is an unusual, expensive operation. It may occasionally be useful as a
way to inspect the contents of
In the logic, this just returns
In the pure ACL2 implementation, the underlying representation of
In the optimized implementation, we similarly need to create a copy of the
current contents of
Function:
(defun nrev$a-copy (nrev$a) (declare (xargs :guard t)) (list-fix nrev$a))
Function:
(defun nrev$c-copy (nrev$c) (declare (xargs :stobjs nrev$c)) (reverse (nrev$c-acc nrev$c)))