<div dir="ltr"><br>Brandon S. Allbery wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><div class="Ih2E3d">
Gwern Branwen wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I've actually long wondered about this: why don't more functions use Nat where it'd make sense? It can't be because Nat is hard to define - I'd swear I've seen many definitions of Nat (if not dozens when you count all the type-level exercises which include one).<br>
</blockquote>
<br></div>
Because naive definitions are dog-slow and fast definitions are anything but easy to use?<br><font color="#888888">
</font></blockquote><div><br>Can you examples of both naive definitions and fast definitions of Nat? I'm curious.<br><br>Sean<br></div></div></div>