9aa723e · Idris-dev · git.iko.soy

libs/prelude/Builtins.idr+2

compare with master

unifiedsplit

@@ -1,3 +1,5 @@

1+%unqualified

2+

1%access public

3%access public

2%default total

4%default total

3

5

libs/prelude/IO.idr+2

@@ -1,3 +1,5 @@

1+%unqualified

2+

1import Prelude.List

3import Prelude.List

2

4

3%access public

5%access public

src/Idris/Parser.hs+3−1

@@ -81,7 +81,9 @@ moduleHeader = try (do reserved "module"

81 i <- identifier

82 option ';' (lchar ';')

83 return (moduleName i))

84+ <|> try (do lchar '%'; reserved "unqualified"

84− <|> return []

85+ return [])

86+ <|> return (moduleName "Main")

85 where moduleName x = case span (/='.') x of

87 where moduleName x = case span (/='.') x of

86 (x, "") -> [x]

88 (x, "") -> [x]

87 (x, '.':y) -> x : moduleName y

89 (x, '.':y) -> x : moduleName y

test/reg003/expected+1−6

@@ -1,7 +1,2 @@

1−reg003a.idr:4:20:When elaborating constructor ECons:

1+reg003a.idr:4:20:When elaborating constructor Main.ECons:

2No such variable OddList

3−reg003a.idr:7:20:When elaborating constructor OCons:

4−No such variable EvenList

5−reg003a.idr:9:8:When elaborating type of test:

6−No such variable EvenList

7−reg003a.idr:10:1:No type declaration for test

test/test010/expected+1−1

@@ -1,3 +1,3 @@

1−test010.idr:13:1:foo is possibly not total due to: MkBad

1+test010.idr:13:1:Main.foo is possibly not total due to: Main.MkBad

2test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad

3test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad