do-notation

[Ben Moseley]

Using Idris 0.9.2.1, the following code:


myact : IO ()
myact = do
putStrLn "Hello"
putStrLn "World"

main : IO ()
main = do
putStrLn "Hello"
putStrLn "World"

-- main : IO ()
-- main = myact


...the version of main which is commented out works fine, but the uncommented version gives a "parse error" at the "do" inside "main".

Is there some special consideration w.r.t. do-notation inside "main" ?

--Ben

[Morel Pisum]

Both versions work here(, I think) with Idris-0.9.3.

Cheers.

[Ben Moseley]

Thanks.

I've just confirmed that it works for me with 0.9.3 too.

--Ben