4 Apr
2008
4 Apr
'08
1:14 p.m.
On Apr 4, 2008, at 11:31 AM, Loup Vaillant wrote:
I mean, could we calculate this equality without reducing length ys to weak head normal form (and then to plain normal form)?
Yes. Suppose equality over Nat is defined something like: Z == Z = True S x == S y = x == y x == y = False And also suppose the length function actually returns a Nat instead of an Int. Now the expression reduces as: length xs == length ys S (length xs') == S (length ys') Z == S (length ys'') False That would not be possible without lazy Nats. - Jake