12 Oct
2006
12 Oct
'06
1:04 a.m.
Nicolas, I think you gave a fine explanation. Just a few minor remarks...
l1 = Cons 3 Nil l2 = Cons 3 _|_
l2 > l1 because l1 is more defined.
Surely you mean l2 < l1, then. Moreover, are you sure you need to define your order in such a way that l2 < l1. I'd say, for these purposes, it's enough to state that (<) = { (_|_, x) | x <- Whnf, x /= _|_ } . But maybe I'm overlooking something here... Cheers, Stefan