[isabelle-dev] Monad_Syntax

Makarius makarius at sketis.net
Wed Sep 11 17:04:02 CEST 2013

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


More information about the isabelle-dev mailing list