Consider:
Inductive [nat:Prop] Constructors [Z:nat][S:nat->nat]; [one = S Z][two = S one][three = S two][four = S three][five = S four]; [add [n,m:nat] = nat_iter ([_:nat]nat) m ([_,x:nat]S x) n];
We add a new non-canonical constant:
[NCC:nat->nat] [||NCC (S(S(S Z))) ==> Z];
(Remark about a minor modification to LEGO rewrite syntax).
In old versions, Hnf NCC two would compute to NCC two. This is reasonable, as NCC two is a whnf (or canonical form): no amount of computation can change its outermost constructor. Similarly, Hnf NCC (add one one) would produce NCC (add one one). However, although NCC two and NCC (add one one) are canonical forms, in order to discover this, LEGO had to compute the arguments two and add one one to S(S Z), and ascertain that this doesn't match with S(S(S Z)), so you might think Hnf NCC (add one one) should produce NCC (S(S Z)), by analogy with beta and projection. For example Hnf (([x:nat->nat]x) f Z), where f is a variable, produces f Z by updating the head of the application, even though the outermost constructor, application, is not changed by this updating. Similarly Hnf (([x:nat#nat]x) f).1 produces f.1. The difference is that beta and projection update the head (root) of an expression, even if they don't change the outer constructor, but rewriting would update the arguments, and not even just "top-level" arguments.
Nonetheless, the original decision not to do pattern updating in LEGO, now seems to have been a poor choice, and the new version does pattern updating.
BTW, notice that in the example above we also have Hnf NCC five returns NCC (S(S(S(S one)))), because LEGO unwinds the argument just far enough to see that it is not three.
Pattern updating brings LEGO's computation very much in line with that of a lazy functional language such as Haskell, except that LEGO's patterns may be non-linear.