		Search-engine friendly clone of the ACL2 documentation.

Rotate-left**

Alternate, recursive definitions of rotate-left.

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

Definitions and Theorems

Theorem: rotate-left**

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

Theorem: rotate-left**-tr

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