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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
