Proof Steps

In order to remove the hard-coding for proof steps such as tactics in Igloo, we propose an ammendment to PGIP:

• element askproofsteps { type_attr? }
  The user interface sends this message to the proof assistant to discover what proof steps are available for use. If type_attr is specified (eg ``tactic'') then the proof assistant only responds with those types of proof steps. Otherwise, all kinds of proof steps are mentioned.

• element addproofstep { type_attr, name_attr, arguments_attr? }
  The proof assistant specifies a proof step, of some type and name, optionally with a list of arguments.

• element addproofsteps { addproofstep+ }
  

  The proof assistant wraps up groups of addproofstep elements with this tag.

These methods may be possible to implement with the opcmd element (see §B.1), but I claim that this syntax is easier to understand.