|
|
|---|
|
|
|
|---|
An extra nrev created with ACL2::defstobj-clone.
This may be useful if you need two nrev stobjs at once.
Definition:
(defabsstobj nrev2 :foundation nrev$c :recognizer (acl2::nrev2p :logic true-listp :exec nrev$cp) :creator (acl2::create-nrev2 :logic create-nrev$a :exec create-nrev$c) :exports ((acl2::nrev-fix2 :logic nrev$a-fix :exec nrev$c-fix$inline :protect nil) (acl2::nrev-copy2 :logic nrev$a-copy :exec nrev$c-copy :protect nil) (acl2::nrev-push2 :logic nrev$a-push :exec nrev$c-push :protect nil) (acl2::nrev-set-hint2 :logic nrev$a-set-hint :exec nrev$c-set-hint :protect nil) (acl2::nrev-finish2 :logic nrev$a-finish :exec nrev$c-finish :protect nil)) :congruent-to nrev)