		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Segment-selectorbits-debug

Signature
(segment-selectorbits-debug x) → *
Arguments: x — Guard (segment-selectorbits-p x).

Definitions and Theorems

Function: segment-selectorbits-debug

(defun segment-selectorbits-debug (x)
  (declare (xargs :guard (segment-selectorbits-p x)))
  (let ((__function__ 'segment-selectorbits-debug))
    (declare (ignorable __function__))
    (b* (((segment-selectorbits x)))
      (cons (cons 'rpl x.rpl)
            (cons (cons 'ti x.ti)
                  (cons (cons 'index x.index) nil))))))