idris-lang/idris-tutorial — pull request #18 by pseudonom (2014-03-07 21:29:01+00:00)
Title: Don't curlify quotes in code environment

Before this change, copying and pasting code from the tutorial resulted in rather subtle curly quotes that Idris balks at. Furthermore, the error Idris throws is pretty uninformative.

```
error: expected: "{",
function declaration
| ( _ ** xs’ ) = if (p x) then ( _ ** x :: xs’ ) else ( _ ** xs’ )
^
```