|
|
|---|
|
|
|
|---|
(cr0bits-debug x) → *
Function:
(defun cr0bits-debug$inline (x) (declare (xargs :guard (cr0bits-p x))) (b* (((cr0bits x))) (cons (cons 'pe x.pe) (cons (cons 'mp x.mp) (cons (cons 'em x.em) (cons (cons 'ts x.ts) (cons (cons 'et x.et) (cons (cons 'ne x.ne) (cons (cons 'res1 x.res1) (cons (cons 'wp x.wp) (cons (cons 'res2 x.res2) (cons (cons 'am x.am) (cons (cons 'res3 x.res3) (cons (cons 'nw x.nw) (cons (cons 'cd x.cd) (cons (cons 'pg x.pg) nil))))))))))))))))