		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))))