		Search-engine friendly clone of the ACL2 documentation.

Nrev-fix

Identity function for nrev.

Signature: (nrev-fix nrev) → nrev'

In the logic, this simply sets:

nrev' := (list-fix nrev)

In both the pure and optimized implementations, this is a no-op that just returns nrev unchanged.

This is a fast operation. It is generally useful to call (nrev-fix nrev) in your function's base case, to avoid needing true-listp hypotheses.

Function: nrev$a-fix

(defun nrev$a-fix (nrev$a)
  (declare (xargs :guard t))
  (list-fix nrev$a))

Function: nrev$c-fix$inline

(defun nrev$c-fix$inline (nrev$c)
  (declare (xargs :stobjs nrev$c))
  nrev$c)