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.