LEGO Version 1.3.1: Known Bugs

Please let us know if you come across any bugs in the current release. We are aware of the following problems:
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.
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.

Last modified: Tue Nov 10 18:25:12 GMT 1998