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

Reply via email to