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
- 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
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