		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logtail

(logtail pos i) returns the high-order part of i, starting at bit position pos.

Signature
(logtail pos i) → int
Arguments: pos — Guard (and (integerp pos) (<= 0 pos)).; i — Guard (integerp i).
Returns: int — Type (integerp int).

In languages like C, this might be written as i >> pos.

Definitions and Theorems

Function: logtail$inline

(defun logtail$inline (pos i)
  (declare (type unsigned-byte pos))
  (declare (xargs :guard (and (and (integerp pos) (<= 0 pos))
                              (integerp i))))
  (declare (xargs :split-types t))
  (let ((__function__ 'logtail))
    (declare (ignorable __function__))
    (mbe :logic (ifloor i (expt2 pos))
         :exec (ash i (- (the unsigned-byte pos))))))

Theorem: logtail-type

(defthm logtail-type
  (b* ((int (logtail$inline pos i)))
    (integerp int))
  :rule-classes :type-prescription)

Subtopics

Ihs/logtail-lemmas: Lemmas about logtail from the logops-lemmas book.
Self-bounds-for-logtail: Lemmas for the bounds of (logtail n a) versus a.
Logtail*: Recursive definition of logtail.