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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
