[isabelle-dev] Monad_Syntax

[Makarius]

On Tue, 20 Aug 2013, Christian Sternagel wrote:

> any opinions on making the type of monadic bind more general (see the 
> attached patch)?

This thread seems to be still open.

Looking at 
http://isabelle.in.tum.de/repos/isabelle/log/73d4c76d8eb2/src/HOL/Library/Monad_Syntax.thy, 
Florian Haftmann and Alex Krauss are the main authors and maintainers of 
this theory.


> "cp >>= f"

Just a marginal question about concrete syntax: I see here various 
alternative notations:

notation (output)
   bind_do (infixr ">>=" 54)

notation (xsymbols output)
   bind_do (infixr "\<guillemotright>=" 54)

notation (latex output)
   bind_do (infixr "\<bind>" 54)

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).


 	Makarius