		Search-engine friendly clone of the ACL2 documentation.

Fast-logext

Fast-logext-fn

Implementation of fast-logext in the general case.

Signature
(fast-logext-fn b x) → *
Arguments: b — Guard (posp b).; x — Guard (integerp x).

Definitions and Theorems

Function: fast-logext-fn

(defun fast-logext-fn (b x)
  (declare (xargs :guard (and (posp b) (integerp x))))
  (let ((__function__ 'fast-logext-fn))
    (declare (ignorable __function__))
    (mbe :logic (logext b x)
         :exec (fast-logext-exec b x))))