Next: Speedups Up: New features in LEGO Version 1.3 Previous: qnify, Qnify and Configure Qnify

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.

Last modified: Tue Jun 23 16:36:46 BST 1998