Major Section: PROOF-CHECKER
Example:
(define-pc-macro ib (&optional term)
(value
(if term
`(then (induct ,term) bash)
`(then induct bash))))
The example above captures a common paradigm: one attempts to prove
the current goal by inducting and then simplifying the resulting
goals. (see proof-checker-commands for documentation of the
command then, which is itself a pc-macro command, and commands
induct and bash.) Rather than issuing (then induct bash), or
worse yet issuing induct and then issuing bash for each resulting
goals, the above definition of ib would let you issue ib and get the
same effect.
General Form: (define-pc-macro cmd args doc-string dcl ... dcl body)where
cmd is the name of the pc-macro than you want to define,
args is its list of formal parameters. Args may include lambda-list
keywords &optional and &rest; see macro-args, but note that
here, args may not include &key or &whole.
The value of body should be an ACL2 ``error triple,'' i.e., have the
form (mv erp xxx state) for some erp and xxx. If erp is
nil, then xxx is handed off to the proof-checker's instruction
interpreter. Otherwise, evaluation typically halts. We may write
more on the full story later if there is interest in reading it.
