		Search-engine friendly clone of the ACL2 documentation.

Sneaky-incf

Sneaky-incf-mutator

Signature
(sneaky-incf-mutator val name-amount) → *
Arguments: val — Guard (consp val).; name-amount — Guard (consp name-amount).

Definitions and Theorems

Function: sneaky-incf-mutator

(defun sneaky-incf-mutator (val name-amount)
  (declare (xargs :guard (and (consp val) (consp name-amount))))
  (declare (xargs :guard (acl2-numberp (cdr name-amount))))
  (let ((__function__ 'sneaky-incf-mutator))
    (declare (ignorable __function__))
    (list (cons (car name-amount)
                (+ (cdr name-amount)
                   (fix (car val)))))))