		Search-engine friendly clone of the ACL2 documentation.

Sneaky

Sneaky-save

Assign a value into the sneaky store.

Signature
(sneaky-save name what) → *

Example:

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

In the logic, sneaky-save just returns nil. Under the hood, we update the sneaky store, e.g., by associating foo with 3.

See also sneaky-mutate for a more general way of manipulating the sneaky store.

Definitions and Theorems

Function: sneaky-save

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

Subtopics

Sneaky-save-mutator