Re: Haskell 2 -- Dependent types?

[Lennart Augustsson]

> > No, the proof (whereever it is) would no longer type check.
> 
> As I understand it, this is not necessarily true:
> if the proof contains loops, it might type check,
> even though it is not really a valid proof.
You're right.  If the proof is looping it will still
pass as a proof.

     -- Lennart