[Haskell-cafe] Clarification on proof section of HS: The Craft of FP

[Jerzy Karczmarczuk]

robert dockins wrote:

>> Assign finite completely defined lists their usual lengths, and every
>> _|_ terminated or infinite list, length w.
>
>
> So every infinite object has a special length denoted "w".  I assume 
> we wish to make the following statements about "w"
>
> w = w
> ~(w < w)
>
> Without which "=" and "<" fail to have their intended meaning.

I don't know what's 'your' intended meaning of the length of an infinite
list, but I don't think you can prove or assume that ~(w<w)

5 < 6
6 < 7
... go to aleph0.

Jerzy Karczmarczuk