idris-lang/Idris-dev — pull request #1137 by reynir (2014-04-30 19:58:00+00:00)
Title: Change 'iota' syntax to allow spaces

For example, [ 1 ..] is allowed but not [ 1 .. ]. That is, "..]" is a token, instead of a ".." token followed by a "]" token. This patch does the latter.