<div dir="ltr"><div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Oct 16, 2013 at 11:46 PM, Yitzchak Gale <span dir="ltr"><<a href="mailto:gale@sefer.org" target="_blank">gale@sefer.org</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div id=":1uc" style="overflow:hidden">I'm not saying that it wouldn't be worthwhile to add a standard<br>
well-optimized implementation of nubOrd somewhere.<br>
But nub is a very useful function. </div></blockquote></div><br>+1<br><br></div>In many cases, an elementary operational semantics beats something more complicated, even if faster.<br><br></div>Please don't kill nub.<br>

<div><br>-- Kim-Ee<div class="gmail_extra">
</div></div></div>