Major Section: PROOF-CHECKER
Example: (define-pc-help pp () (if (goals t) (io? proof-checker nil state (state-stack) (fms0 "~|~y0~|" (list (cons #0 (fetch-term (conc t) (current-addr t)))))) (print-all-goals-proved-message state)))This defines a macro command named
General Form: (define-pc-help name args &rest body)
name, as explained further below. The
bodyshould (after removing optional declarations) be a form that returns
stateas its single value. Typically, it will just print something.
(define-pc-help name args &rest body) really does is to create
a call of
define-pc-macro that defines
name to take arguments
to have the declarations indicated by all but the last form in
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
(which will return
(mv nil t state)).