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

[Henning Thielemann]

On Mon, 2 May 2005, Daniel Carrera wrote:

> Daniel Fischer wrote:
>
>> Both do, but in Explanation 2, you omitted 'finite' a couple of times.
>
> Well, I also omited the word "countable". I figure it's understood since 
> computers only deal with finite data. And given an infinite list, any finite 
> "head" of it would meet the criteria, so the distinction is moot. Unless 
> Haskell has some neat property I am not aware of :-)

If you don't take care you may end up "proving" that e.g.
   repeat 1 ++ [0]  ==  repeat 0
  because for the first list you can prove that every reachable element is 
equal to its neighbour and the "last" element is 0.