LEGO Version 1.3: Known Bugs

Cd

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

Double

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

Expansion

The command ExpAll no longer works.

Freezing

Freezing terms while constructing a proof may lead to problems in building the internal partial proof tree and LEGO fails with *tocAppErr*.

Pwd

under Linux does not work.

Induction

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

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.