git.iko.soy/Idris-dev
on master help sign in
Change 'iota' syntax to allow spaces

For example, [ 1 ..] was allowed but not [ 1 .. ]. That is, "..]" was a token, and now it's ".." followed by "]".

commita787da0d3c9763fc32a51496ea3e5a182bed9260 authorReynir Björnsson <reynir@reynir.dk> dateMon 28 Apr 2014, 14:24 (13 years ago) parent62705e4
1 file changed+2−2
compare with master
unifiedsplit
libs/prelude/Prelude.idr+2−2
libs/prelude/Prelude.idr+2−2
@@ -412,9 +412,9 @@ syntax "[" [start] ".." [end] "]"
412412syntax "[" [start] "," [next] ".." [end] "]"
413413 = enumFromThenTo start (next - start) end
414414
415−syntax "[" [start] "..]"
415+syntax "[" [start] ".." "]"
416416 = enumFrom start
417−syntax "[" [start] "," [next] "..]"
417+syntax "[" [start] "," [next] ".." "]"
418418 = enumFromThen start (next - start)
419419
420420---- More utilities