Re: [isabelle] Haskabelle configuration

Hi Andreas,

> 2. do notation
> Apparently, Haskabelle has some undocumented support for do notation and
> monads. At least, this is what I gather from the files in ex/ and the
> error message for the following program:
> f = do {
>   x <- [1,2];
>   y <- [x + 1];
>   [y]
> }
> haskabelle_bin: Do syntax is used without sufficient type information!
> What type information do I have to add (and where) such that such
> examples compile? Actually, I would have expected that no type
> information were necessary, because Isabelle's parser setup for do
> notation in Library/Monad_Syntax should resolve the operations correctly.
> Can I configure Haskabelle to use that setup?

maybe Gerwin can point you to some reference – that do-notation
extension was developed at NICTA, AFAIR.



PGP available:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.