[isabelle-dev] Monad_Syntax

[Alexander Krauss]

Hi Chris,

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

Generalizing bind itself would rather be a topic for ICFP or POPL, and I 
cannot comment on that :-) Concerning the constant that represents it 
syntactically, I would say that if it does not break anything then it is 
fine. After all, this is just ad-hoc overloading, so generalizations can 
also be ad-hoc.

> I tested the change against IsaFoR (which makes heavy use of
> Monad_Syntax). Unfortunately, running JinjaThreads (which also uses
> Monad_Syntax) timed out on my machine (hopefully not due to the patch).
> Could anybody with access to a more powerful machine check this please?

Pushed to testboard, which should run it on decent hardware:
http://isabelle.in.tum.de/testboard/Isabelle/rev/eeff8139b3d8

Alex