<br><div class="gmail_quote">On Mon, Apr 23, 2012 at 10:28 AM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@chalmers.se">nad@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On 2012-04-23 09:07, Andreas Abel wrote:<br>
</div><div class="im"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Mmh, the easiest fix is: trash the builtin NATDIVSUCAUX. I do not know what it is for. The only use I found for it was in<br>
<br>
example/lib/Data/Nat.agda<br>
<br>
with the definition you have given below.<br>
</blockquote>
<br></div><div class="im">
See <a href="http://code.google.com/p/agda/issues/detail?id=172" target="_blank">http://code.google.com/p/agda/<u></u>issues/detail?id=172</a> for some context.<br></div></blockquote><div> </div><div>The purpose is to give you fast (=running on Haskell integers) div and mod on nats</div>
<div>at compile time.</div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">By the way, I'm not surprised that people manage to wreak havoc by using</div>
BUILTINs, in many cases the sanity checking for BUILTINs is less than<br>
optimal. I think the idea is that you should only use BUILTINs (and<br>
postulates, and the FFI) if you know what you are doing.</blockquote><div><br></div><div>The sanity checking for BUILTINs is supposed to disallow incorrect definitions,</div><div>if it doesn't it's a bug that should be fixed. The FFI and postulates obviously let</div>
<div>you "prove" whatever you want, but BUILTINs shouldn't.</div><div><br></div><div>/ Ulf</div></div>