define a macro command whose purpose is to print something
Major Section:  PROOF-CHECKER

(define-pc-help pp () 
  (if (goals t)
      (io? proof-checker nil state
           (fms0 "~|~y0~|"
                 (list (cons #0 
                             (fetch-term (conc t)
                                         (current-addr t))))))
    (print-all-goals-proved-message state)))

General Form:
(define-pc-help name args &rest body)
This defines a macro command named name, as explained further below. The body should (after removing optional declarations) be a form that returns state as its single value. Typically, it will just print something.

What (define-pc-help name args &rest body) really does is to create a call of define-pc-macro that defines name to take arguments args, to have the declarations indicated by all but the last form in body, and to have a body that (via pprogn) first executes the form in the last element of body and then returns a call to the command skip (which will return (mv nil t state)).