		Search-engine friendly clone of the ACL2 documentation.

Sneaky

Sneaky-pop

Pop the car off a list in the sneaky store.

Signature
(sneaky-pop name) → *

Example:

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

In the logic, sneaky-pop just returns nil. Under the hood, we update the sneaky store, removing the first element of the value of name.

Definitions and Theorems

Function: sneaky-pop

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

Subtopics

Sneaky-pop-mutator