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