DEFINE-PC-MACRO

define a proof-checker macro command 
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 error triple (see error-triples), of 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.