[isabelle-dev] Monad_Syntax

[Makarius]

On Wed, 11 Sep 2013, Florian Haftmann wrote:

>> Do monadic people have a standard Unicode point to render that operator?
>> If yes, we could assign that to \<bind> and use it from STIX (or provide
>> a glyph in the IsabelleText font).
>
> For LaTeX I once have been using 
> \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}} 
> following a suggestion by Jasmin as far as I remember.

We have the latex macro already since Isabelle/a33ecf47f0a0 (haftmann 
2010).

If we find some Unicode point for it, we could reduce the variance of 
notation to 2 or even 1.  Allocating Unicode slots is a sport of many 
subcultures, e.g. people writing text in Klingon (they did not make it 
into the official charts, yet).

Looking around in Deja Vu or STIX for a few minutes, I did not find 
anything like \<bind> yet, but it might be still there hidden within 
thousands of symbols.


 	Makarius