Shape matcher code review #42
ice1000Annotations
5 errors
|
LibraryTest.fastTestOnDisk():
base/src/test/java/org/aya/test/LibraryTest.java#L53
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.PatternProblem$BadLitPattern`: In file List2.aya:9:2 ->
7 |
8 | def simpleMatch (x : SomeList {Nat}) : SomeList {Nat}
9 | | [ ] => empty
| ^-^
Error: The literal
[ ]
cannot be encoded as a term of type:
SomeList {Nat}
at (278-280) [9,2-9,4]
|
|
LibraryTest.testInMemoryAndPrim():
base/src/test/java/org/aya/test/LibraryTest.java#L78
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.PatternProblem$BadLitPattern`: In file List2.aya:9:2 ->
7 |
8 | def simpleMatch (x : SomeList {Nat}) : SomeList {Nat}
9 | | [ ] => empty
| ^-^
Error: The literal
[ ]
cannot be encoded as a term of type:
SomeList {Nat}
at (278-280) [9,2-9,4]
|
|
LibraryTest.[1] success:
base/src/test/java/org/aya/test/LibraryTest.java#L44
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.PatternProblem$BadLitPattern`: In file List2.aya:9:2 ->
7 |
8 | def simpleMatch (x : SomeList {Nat}) : SomeList {Nat}
9 | | [ ] => empty
| ^-^
Error: The literal
[ ]
cannot be encoded as a term of type:
SomeList {Nat}
at (278-280) [9,2-9,4]
|
|
LibraryTest.testLiterate():
base/src/test/java/org/aya/test/LibraryTest.java#L64
java.lang.AssertionError: Failed with `class org.aya.tyck.pat.PatternProblem$BadLitPattern`: In file List2.aya:9:2 ->
7 |
8 | def simpleMatch (x : SomeList {Nat}) : SomeList {Nat}
9 | | [ ] => empty
| ^-^
Error: The literal
[ ]
cannot be encoded as a term of type:
SomeList {Nat}
at (278-280) [9,2-9,4]
|
|
TestRunner.runAllAyaTests():
base/src/test/java/org/aya/test/TestRunner.java#L50
org.opentest4j.AssertionFailedError: implicit-element-list-pattern.aya ==> expected: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya:11:8 ->
9 │ def bad {A : Type} (xs : List A) (default : A) : A
10 │ | nil, default => default
11 │ | [ _, {y} ], default => y
│ ╰╯
Error: Implicit elements in a list pattern is disallowed
1 error(s), 0 warning(s).
What are you doing?
> but was: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya:11:8 ->
9 │ def bad {A : Type} (xs : List A) (default : A) : A
10 │ | nil, default => default
11 │ | [ _, {y} ], default => y
│ ╰╯
Error: Implicit elements in a list pattern is disallowed
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya:6:2 ->
4 │ def good {A : Type} (xs : List A) (default : A) : A
5 │ | nil, default => default
6 │ | [ _, y ], default => y
│ ╰──────╯
Error: The literal
[ _, y ]
cannot be encoded as a term of type:
List A
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya:11:2 ->
9 │ def bad {A : Type} (xs : List A) (default : A) : A
10 │ | nil, default => default
11 │ | [ _, {y} ], default => y
│ ╰────────╯
Error: The literal
[ _, y ]
cannot be encoded as a term of type:
List A
3 error(s), 0 warning(s).
What are you doing?
>
|