<div dir="ltr"><div class="gmail_extra">The first example was meant to be <font face="monospace, monospace">[ a, b ]</font><font face="arial, helvetica, sans-serif">. Sorry.</font></div></div>