		Search-engine friendly clone of the ACL2 documentation.

Sneaky-push

Sneaky-push-mutator

Signature
(sneaky-push-mutator previous name-head) → *
Arguments: previous — Guard (consp previous).; name-head — Guard (consp name-head).

Definitions and Theorems

Function: sneaky-push-mutator

(defun sneaky-push-mutator (previous name-head)
  (declare (xargs :guard (and (consp previous)
                              (consp name-head))))
  (let ((__function__ 'sneaky-push-mutator))
    (declare (ignorable __function__))
    (list (cons (car name-head)
                (cons (cdr name-head)
                      (car previous))))))