I don&#39;t think there&#39;s an easy way to check. Not-obviously-terminating definitions will get marked in pink if typechecking completes, but if you go and use one directly in a type somewhere and the definition really doesn&#39;t terminate on the input in the type, then the typechecker won&#39;t terminate. So if you use possibly non-terminating functions in types, you might want to split up your file to make sure nothing that would normally be pink is hanging your typechecker.<div>
<br></div><div>The other time I&#39;ve seen things hang is when you use recursive records. You might want to check that you don&#39;t have any of those, either.</div><div><br></div><div>Other than that, I don&#39;t have too many ideas :(<br>
<br><div class="gmail_quote">On Thu, Jul 5, 2012 at 12:02 PM, Ondrej Rypacek <span dir="ltr">&lt;<a href="mailto:ondrej.rypacek@gmail.com" target="_blank">ondrej.rypacek@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi all<br>
<br>
Is there a way to tell if Agda is going to halt on my program? It&#39;s been crunching for more than 24 hours now, on a more or less constant memory use.<br>
<br>
Is there a way to tell if there&#39;s a point in keeping it alive?<br>
<br>
Cheers,<br>
Ondrej_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>