		Search-engine friendly clone of the ACL2 documentation.

Sneaky

Sneaky-load

Load a value that was previously saved into the sneaky store.

Signature
(sneaky-load name state) → (mv value state)

Example:

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

In the logic, this function reads from the ACL2 oracle. Under the hood, we redefine it so that it reads from a hash table and allows you to access the values saved by, e.g., sneaky-save and sneaky-push.

Definitions and Theorems

Function: sneaky-load

(defun sneaky-load (name state)
  (declare (xargs :stobjs (state)))
  (declare (ignore name))
  (declare (xargs :guard t))
  (let ((__function__ 'sneaky-load))
    (declare (ignorable __function__))
    (b* ((- (raise "Under-the-hood definition not yet installed"))
         ((mv ?err val state)
          (read-acl2-oracle state)))
      (mv val state))))