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
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|
|10.2 LEGO tags|
|10.3 LEGO customizations|
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
- C-c C-a C-I
- C-c C-a C-R
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
This document was generated by Erik Martin-Dorel on April 2, 2020 using texi2html 1.82.