[gathering-options] Arrow symbol

[Mark Thornton]

On 22/06/11 14:43, Stephen Colebourne wrote:
> Use ->
>    {x ->   x + 1}
>    (x) ->   {x + 1}
>
> Use =>
>    {x =>   x + 1}
>    (x) =>   {x + 1}
>
>
To save others the trouble here are the obvious unicode arrows

Use ?
   {x ?  x + 1}
   (x) ?  {x + 1}

Use ?
   {x ?  x + 1}
   (x) ?  {x + 1}

(with a larger arrow font size)
   {x?   x + 1}
   (x)?   {x + 1}



Doesn't look that good in the font/size shown above

Mark