LEGO Rewrite Syntax

In previous LEGO versions

[NCC three ==> Z]
was not valid syntax; even if the rule contained no match variables, a match variable context was required, as in
[[_:nat]NCC (S(S(S Z))) ==> Z]
Rewrites without a match variable context are now accepted if the first equation is preceeded by the choice operator ||, so
[||NCC (S(S(S Z))) ==> Z]
is accepted.

Last modified: 13-Feb-1997