		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)))))