		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Gdtr/idtrbits-debug

Signature
(gdtr/idtrbits-debug x) → *
Arguments: x — Guard (gdtr/idtrbits-p x).

Definitions and Theorems

Function: gdtr/idtrbits-debug

(defun gdtr/idtrbits-debug (x)
  (declare (xargs :guard (gdtr/idtrbits-p x)))
  (let ((__function__ 'gdtr/idtrbits-debug))
    (declare (ignorable __function__))
    (b* (((gdtr/idtrbits x)))
      (cons (cons 'base-addr x.base-addr)
            (cons (cons 'limit x.limit) nil)))))