<div dir="auto"><div>But they *are* ordered. Otherwise, comparison of two maps would be undefined. </div><div dir="auto"><br></div><div dir="auto">BR, </div><div dir="auto">Ulf W<br><div class="gmail_extra" dir="auto"><br><div class="gmail_quote">Den 26 okt. 2017 18:20 skrev "Roger Lipscombe" <<a href="mailto:roger@differentpla.net">roger@differentpla.net</a>>:<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="quoted-text">On 26 October 2017 at 16:30, Ulf Wiger <<a href="mailto:ulf@wiger.net">ulf@wiger.net</a>> wrote:<br>
> Wouldn't it be reasonable to have such a function?<br>
<br>
</div>First thought: No, because people would start abusing it. Maps *aren't* ordered.<br>
</blockquote></div><br></div></div></div>