		Search-engine friendly clone of the ACL2 documentation.

Sneaky

Sneaky-cw

Print a value from the sneaky store.

Signature
(sneaky-cw name) → *

Example:

(sneaky-save 'foo 3)
(sneaky-cw 'foo)     ; prints 3, returns nil

In the logic, sneaky-cw just returns nil. Under the hood, we look up the value of name in the sneaky store and print it to the comment window, e.g., using cw.

Definitions and Theorems

Function: sneaky-cw

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

Subtopics

Sneaky-cw-mutator