		Search-engine friendly clone of the ACL2 documentation.

Logrev

Logrev1

Helper function for logrev.

Signature
(logrev1 size i j) → nat
Arguments: size — Guard (and (integerp size) (<= 0 size)).; i — Guard (integerp i).; j — Guard (integerp j).

Definitions and Theorems

Function: logrev1

(defun logrev1 (size i j)
  (declare (xargs :guard (and (and (integerp size) (<= 0 size))
                              (integerp i)
                              (integerp j))))
  (declare (type unsigned-byte size)
           (type integer i j))
  (declare (xargs :split-types t))
  (let ((__function__ 'logrev1))
    (declare (ignorable __function__))
    (if (zp size)
        (mbe :logic (ifix j) :exec j)
      (logrev1 (the unsigned-byte (- size 1))
               (logcdr i)
               (logcons (logcar i) j)))))