LEGO Version 1.3: Relaxed Patterns and Inductive Types

The previous version of LEGO did not support lambda-abstractions on the right hand side of patterns, which meant that the reduction rules for certain inductive types were not automatically generated. This has now been fixed.

For example, accessibility (locally noetherian) can be defined without the "NoReductions" keyword.

  Init XCC; [TYPE=Prop][A:Prop][R:A->A->Prop];
  Inductive [lnoth:A->Prop]
    Constructors [ln:{a|A}({b|A}(R a b)->lnoth b)->lnoth a];

NoReductions is probably only useful now for backwards compatability.