Removed Unicode character from source file

Unicode is discouraged according to
https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291