Major Section: PROOF-CHECKER
Example:
(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)).
