		Search-engine friendly clone of the ACL2 documentation.

Sneaky

Sneaky-push

Extend a value in the sneaky store.

Signature
(sneaky-push name what) → *

Example:

(sneaky-save 'foo '(3))
(sneaky-push 'foo 4)
(sneaky-load 'foo state) --> (mv '(4 3) state)

In the logic, sneaky-push just returns nil. Under the hood, we update the sneaky store, updating name by "pushing" a new value onto its current value. The accumulated values can later be accessed with sneaky-load. See also sneaky-save.

Definitions and Theorems

Function: sneaky-push

(defun sneaky-push (name what)
  (declare (xargs :guard t))
  (let ((__function__ 'sneaky-push))
    (declare (ignorable __function__))
    (sneaky-mutate 'sneaky-push-mutator
                   (list name)
                   (cons name what))))

Subtopics

Sneaky-push-mutator