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.