		Search-engine friendly clone of the ACL2 documentation.

Sneaky

Sneaky-alist

Load an alist containing all values previously saved into the sneaky store.

Signature
(sneaky-alist state) → (mv alist state)

Example:

(sneaky-save 'foo 3)
(sneaky-alist state) --> (mv '((foo . 3)) state)

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

Definitions and Theorems

Function: sneaky-alist

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