		Search-engine friendly clone of the ACL2 documentation.

Modr/m-structures

Modr/m-debug

Signature
(modr/m-debug x) → *
Arguments: x — Guard (modr/m-p x).

Definitions and Theorems

Function: modr/m-debug$inline

(defun modr/m-debug$inline (x)
  (declare (xargs :guard (modr/m-p x)))
  (b* (((modr/m x)))
    (cons (cons 'r/m x.r/m)
          (cons (cons 'reg x.reg)
                (cons (cons 'mod x.mod) nil)))))