> If you return the same proof of correctness that you used
> for the earlier definition of sort, then no it won't type check.
> But if you return a proof defined as e.g.
> 
>       proof = proof
> 
> then if I understand things correctly it will type check.

On that note, since this has been of interest on comp.lang.functional:

Howabout a way to tell the compiler: "don't allow general recursion"? 


Reply via email to