Define-pc-help
Define a macro command whose purpose is to print something
Example:
(define-pc-help pp ()
(if (goals t)
(io? proof-builder nil state
(state-stack)
(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)).
