LEGO Version 1.3.1: Known Bugs

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.

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.