Irrefutable Lambda #702
HoshinoTentedAnnotations
4 errors
|
LibraryTest.testInMemoryAndPrim():
cli-impl/src/test/java/org/aya/test/LibraryTest.java#L94
java.lang.AssertionError: Failed with `class org.aya.tyck.error.PatternProblem$UnknownCon`: In file relation/binary/path.aya:11:61 ->
9 | def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
10 |
11 | def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
| ^^
Error: Unknown constructor
i
at (340-340) [11:61-11:61]
|
|
LibraryTest.[1] success:
cli-impl/src/test/java/org/aya/test/LibraryTest.java#L55
java.lang.AssertionError: Failed with `class org.aya.tyck.error.PatternProblem$UnknownCon`: In file relation/binary/path.aya:11:61 ->
9 | def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
10 |
11 | def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
| ^^
Error: Unknown constructor
i
at (340-340) [11:61-11:61]
|
|
LibraryTest.testLiterate():
cli-impl/src/test/java/org/aya/test/LibraryTest.java#L72
java.lang.AssertionError: Failed with `class org.aya.tyck.error.PatternProblem$UnknownCon`: In file relation/binary/path.aya:11:61 ->
9 | def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
10 |
11 | def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
| ^^
Error: Unknown constructor
i
at (340-340) [11:61-11:61]
|
|
TestRunner.negative():
cli-impl/src/test/java/org/aya/test/TestRunner.java#L59
org.opentest4j.AssertionFailedError: diff --git a/cli-impl/src/test/resources/negative/ParseError.txt b/cli-impl/src/test/resources/negative/ParseError.txt
index 1e18b50..67586c5 100644
--- a/cli-impl/src/test/resources/negative/ParseError.txt
+++ b/cli-impl/src/test/resources/negative/ParseError.txt
@@ -109,7 +109,18 @@ In file $FILE:4:4 ->
Error: Implicit elements in a list pattern is disallowed
-1 error(s), 0 warning(s).
+In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/relation/binary/path.aya:11:61 ->
+
+ 9 │ def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
+ 10 │
+ 11 │ def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
+ │ ╰╯
+
+Error: Unknown constructor
+ i
+
+Resolving interrupted due to:
+2 error(s), 0 warning(s).
Let's learn from that.
IncorrectReturn:
==> expected: <true> but was: <false>
|