		Search-engine friendly clone of the ACL2 documentation.

Nrev

Nrev-stobj

Definition of the nrev abstract stobj.

Definition: nrev

(defabsstobj nrev
  :foundation nrev$c
  :recognizer (nrev$p :logic true-listp :exec nrev$cp)
  :creator (acl2::create-nrev :logic create-nrev$a
                              :exec create-nrev$c)
  :corr-fn nrev-corr
  :exports ((nrev-fix :logic nrev$a-fix
                      :exec nrev$c-fix$inline)
            (nrev-copy :logic nrev$a-copy
                       :exec nrev$c-copy)
            (nrev-push :logic nrev$a-push
                       :exec nrev$c-push)
            (nrev-set-hint :logic nrev$a-set-hint
                           :exec nrev$c-set-hint)
            (nrev-finish :logic nrev$a-finish
                         :exec nrev$c-finish)))

Definitions and Theorems

Function: create-nrev$a

(defun create-nrev$a nil
  (declare (xargs :guard t))
  nil)

Function: nrev-corr

(defun nrev-corr (nrev$c nrev$a)
  (declare (xargs :stobjs nrev$c))
  (equal (nrev$c-copy nrev$c)
         (nrev$a-copy nrev$a)))