idris-lang/Idris-dev — pull request #1660 by david-christiansen (2014-10-18 18:50:34+00:00)
Title: Make do blocks require an expression

This makes for better error messages and fixes #1656.

Old message:

> :t do
When elaborating an application of constructor __infer:
INTERNAL ERROR: Invalid statement in do block
This is probably a bug, or a missing error message.
Please consider reporting at
https://github.com/idris-lang/Idris-dev/issues

New message:

> :t do
(input):1:6: error: unexpected
EOF, expected: ")",
do block expression,
end of "do", start of block
:t do