On Thu, Apr 3, 2008 at 11:13 PM, Don Stewart <<a href="mailto:dons@galois.com">dons@galois.com</a>> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">length, take, drop and index working on machine-sized Ints by default<br>
are really a bit of a wart, aren't they?<br>
<font color="#888888"><br>
-- Don</font></blockquote><br>
Agreed,<br>
<br>
Olivier.