## 10 LEGO Proof General

LEGO proof script mode is a mode derived from proof script mode for editing LEGO scripts. An important convention is that proof script buffers must start with a module declaration. If the proof script buffer’s file name is `fermat.l`, then it must commence with a declaration of the form

    Module fermat;

If, in the development of the module ‘`fermat`’, you require material from other module e.g., ‘`lib_nat`’ and ‘`galois`’, you need to specify this dependency as part of the module declaration:

    Module fermat Import lib_nat galois;

No need to worry too much about efficiency. When you retract back to a module declaration to add a new import item, LEGO does not actually retract the previously imported modules. Therefore, reasserting the extended module declaration really only processes the newly imported modules.

Using the LEGO Proof General, you never ever need to use administrative LEGO commands such as ‘`Forget`’, ‘`ForgetMark`’, ‘`KillRef`’, ‘`Load`’, ‘`Make`’, ‘`Reload`’ and ‘`Undo`’ again 7.

### 10.1 LEGO specific commands

In addition to the commands provided by the generic Proof General (as discussed in the previous sections) the LEGO Proof General provides a few extensions. In proof scripts, there are some abbreviations for common commands:

`C-c C-a C-i`

  intros

`C-c C-a C-I`

  Intros

`C-c C-a C-R`

  Refine

### 10.2 LEGO tags

You might want to ask your local system administrator to tag the directories `lib_Prop`, `lib_Type` and `lib_TYPE` of the LEGO library. See Support for tags, for further details on tags.

### 10.3 LEGO customizations

We refer to chapter Customizing Proof General, for an introduction to the customisation mechanism. In addition to customizations at the generic level, for LEGO you can also customize:

User Option: lego-tags

  The directory of the tags table for the lego library

  The default value is `"/usr/lib/lego/lib_Type/"`.

Variable: lego-www-home-page

  Lego home page URL.

#### Footnotes

### (7)

And please, don’t even think of including those in your LEGO proof script!