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
later arguments may lead to illegal reduction rules, thus
corrupting the object file.
Last modified: Tue Nov 10 18:25:12 GMT 1998