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.
Florian Haftmann and Alex Krauss are the main authors and maintainers of
> "cp >>= f"
Just a marginal question about concrete syntax: I see here various
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