Next: Coq Proof General, Previous: Hints and Tips, Up: Top [Contents][Index]
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.
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:
intros
Intros
Refine
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.
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:
The directory of the tags table for the lego library
The default value is "/usr/lib/lego/lib_Type/"
.
Lego home page URL.
Previous: LEGO tags, Up: LEGO Proof General [Contents][Index]