		Search-engine friendly clone of the ACL2 documentation.

Rotate-right**

Alternate, recursive definitions of rotate-right.

Here are both tail-recursive and non tail-recursive versions of rotate-right. These rules are disabled by default and must be explicitly enabled when you want to use them.

Definitions and Theorems

Theorem: rotate-right**

(defthm
     rotate-right**
     (equal (rotate-right x width places)
            (if (zp places)
                (loghead width x)
                (rotate-right-1 (rotate-right x width (- places 1))
                                width)))
     :rule-classes
     ((:definition :clique (rotate-right)
                   :controller-alist ((rotate-right nil nil t)))))

Theorem: rotate-right**-tr

(defthm
     rotate-right**-tr
     (equal (rotate-right x width places)
            (if (zp places)
                (loghead width x)
                (rotate-right (rotate-right-1 x width)
                              width (- places 1))))
     :rule-classes
     ((:definition :clique (rotate-right)
                   :controller-alist ((rotate-right nil nil t)))))