Proofs and development
Marko van Eekelen
marko@cs.kun.nl
Thu, 4 Jun 1998 09:29:57 +0200
Adrian Hey wrote:
>
> Reverse (Reverse [1,2..]) = _|_, which isn't equivalent to [1,2..]
>
>Have you decided what implications this has for the use of this kind of
>theorem prover with Clean, or is it too early to ask this question?
>
Dear Adrian,
Of course, this stuff only works for finite lists. It is a problem all theorem provers have to face. The theory is very different for finite and for infinite lists. So, you would expect that there will be a way to make the distinction between the two. But, as you suggest, it is a bit too early to decide on concrete implications for Clean.
Regards,
Marko van Eekelen.