LEGO Version 1.3: Known Bugs

Please let us know if you come across any bugs in the current release. We are aware of the following problems:
Under Linux, the command Cd always complains about an uncaught exception, despite actually changing the directory. [This will be fixed in the version 1.3.1.]
The computation of double elimination rules uses named variables. If an inductive definition uses a name twice or a name used by the system, the clash may cause an error. Workaround: do not duplicate names and never call anything "z".
The command ExpAll no longer works.
Freezing terms while constructing a proof may lead to problems in building the internal partial proof tree and LEGO fails with *tocAppErr*.
under Linux does not work.
Induction currently fails for some parameterised families of inductive types (eg lists). [This will be fixed in the version 1.3.1.]
Local Definitions, Reductions and Discharge
Reduction rules containing local definitions are rejected by the reduction compiler. A valid reduction rule which refers to a locally defined variable will become invalid when that variable is discharged.
Qnify sometimes does not perform all the reduction it should, hence ignoring equations it is intended to process. [This will be fixed in the version 1.3.1.]
Reduction Rules
Implicit arguments in constructors which cannot actually be inferred from later arguments may lead to illegal reduction rules, thus corrupting the object file. In addition, certain kinds of legitimate reduction rules may be incorrectly parsed on reloading: to work around this, add more brackets by hand.

Last modified: Sat Oct 24 12:52:25 BST 1998