		Search-engine friendly clone of the ACL2 documentation.

Sneaky

Sneaky-incf

Increment a value in the sneaky store.

Signature
(sneaky-incf name &optional (amount '1)) → *
Arguments: amount — Guard (acl2-numberp amount).

Example:

(sneaky-save 'foo 3)
(sneaky-incf 'foo)   ;; increment by 1
(sneaky-incf 'foo 2) ;; increment by 2
(sneaky-load 'foo state) --> (mv 6 state)

In the logic, sneaky-incf just returns nil. Under the hood, we update the sneaky store, incrementing the value of name by the indicated amount. The accumulated values can later be accessed with sneaky-load. See also sneaky-save.

Definitions and Theorems

Function: sneaky-incf-fn

(defun sneaky-incf-fn (name amount)
  (declare (xargs :guard (acl2-numberp amount)))
  (let ((__function__ 'sneaky-incf))
    (declare (ignorable __function__))
    (sneaky-mutate 'sneaky-incf-mutator
                   (list name)
                   (cons name amount))))

Subtopics

Sneaky-incf-mutator