Std lib updates #584
ice1000Annotations
4 errors
|
LibraryTest.testInMemoryAndPrim():
cli-impl/src/test/java/org/aya/test/LibraryTest.java#L88
java.lang.AssertionError: Failed with `class org.aya.resolve.error.NameProblem$QualifiedNameNotFoundError`: In file data/list/base.aya:3:38 ->
1 | open import arith::nat::base
2 | open import relation::binary::path
3 | open import data::maybe using (Maybe, Just, Nothing)
| ^--^
Error: The qualified name `data::maybe::Just` is not defined in the current
scope
at (102-105) [3:38-3:41]
|
|
LibraryTest.[1] success:
cli-impl/src/test/java/org/aya/test/LibraryTest.java#L53
java.lang.AssertionError: Failed with `class org.aya.resolve.error.NameProblem$QualifiedNameNotFoundError`: In file data/list/base.aya:3:38 ->
1 | open import arith::nat::base
2 | open import relation::binary::path
3 | open import data::maybe using (Maybe, Just, Nothing)
| ^--^
Error: The qualified name `data::maybe::Just` is not defined in the current
scope
at (102-105) [3:38-3:41]
|
|
LibraryTest.testLiterate():
cli-impl/src/test/java/org/aya/test/LibraryTest.java#L74
java.lang.AssertionError: Failed with `class org.aya.resolve.error.NameProblem$QualifiedNameNotFoundError`: In file data/list/base.aya:3:38 ->
1 | open import arith::nat::base
2 | open import relation::binary::path
3 | open import data::maybe using (Maybe, Just, Nothing)
| ^--^
Error: The qualified name `data::maybe::Just` is not defined in the current
scope
at (102-105) [3:38-3:41]
|
|
TestRunner.negative():
cli-impl/src/test/java/org/aya/test/TestRunner.java#L48
org.opentest4j.AssertionFailedError: ParseError.txt ==> expected: <Trivial:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:0 ->
1 │ def
│ ╰─╯
Error: Expect a name
1 error(s), 0 warning(s).
Let's learn from that.
Modifier:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:0 ->
1 │ overlap inductive E
│ ╰─────╯
Error: The modifier overlap is not suitable here.
1 error(s), 0 warning(s).
Let's learn from that.
IgnoredModifier:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:0 ->
1 │ inline def id {A : Type} A : A
│ ╰────╯
2 │ | a => a
Warning: Ignoring inline
That looks right!
OverlapOnExpr:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:0 ->
1 │ overlap def id {A : Type} (a : A) => a
│ ╰─────╯
Warning: The modifier overlap is redundant, ignored.
That looks right!
IgnorePragma:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:1 ->
1 │ @thisWillNeverBeARealPragma
│ ╰────────────────────────╯
2 │ def id {A : Type} (a : A) => a
Warning: Unrecognized pragma `thisWillNeverBeARealPragma` will be ignored.
That looks right!
IgnoreSuppressed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:10 ->
1 │ @Suppress(thisWillNeverBeARealWarning)
│ ╰─────────────────────────╯
2 │ def id {A : Type} (a : A) => a
Warning: Unrecognized warning `thisWillNeverBeARealWarning` will be ignored.
That looks right!
MatchElim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->
1 │ def test => match elim Type {}
│ ╰────────────────╯
Error: Elimination match must be on variables
Parsing interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
MatchNumMismatch:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->
1 │ def test => match e as a, b returns Type {}
│ ╰─────────────────────────────╯
Error: I see 2 as-binding(s) but 1 discriminant(s)
Parsing interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImplicitTuplePat:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:3 ->
1 │ def test (Sig Type ** Type) : Type
2 │ | ({a}, b) => a
│ ╰─╯
Error: Implicit pattern is not allowed here.
1 error(s), 0 warning(s).
Let's learn from that.
ImplicitListPat:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:3 ->
2 │ open import arith::nat::base
3 │ def test (List Nat) : Nat
4 │ | [{a}] => a
│ ╰─╯
Error: Implicit elements in a list pattern is disallowed
1 error(s), 0 warning(s).
Let's learn from that.
> but was: <Trivial:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:0 ->
1 │ def
│ ╰─╯
Error: Expect a name
1 error(s), 0 warning(s).
Let's learn from that.
Modifier:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:0 ->
1 │ overlap inductive E
│ ╰─────╯
Error: The modifier overlap is not suitable here.
1 error(s), 0 warning(s).
Let's learn from that.
IgnoredModifier:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:0 ->
1 │ inline def id {A : Type} A : A
│ ╰────╯
2 │ | a => a
Warning: Ignoring inline
That looks right!
OverlapOnExpr:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:0 ->
1 │ overlap def id {A : Type} (a : A) => a
│ ╰─────╯
Warning: The modifier overlap is redundant, ignored.
That looks right!
IgnorePragma:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:1 ->
1 │ @thisWillNeverBeARealPragma
│ ╰────────────────────────╯
2 │ def id {A : Type} (a : A) => a
Warning: Unrecognized pragma `thisWillNeverBeARealPragma` will be ignored.
That looks right!
IgnoreSuppressed:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:10 ->
1 │ @Suppress(thisWillNeverBeARealWarning)
│ ╰─────────────────────────╯
2 │ def id {A : Type} (a : A) => a
Warning: Unrecognized warning `thisWillNeverBeARealWarning` will be ignored.
That looks right!
MatchElim:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->
1 │ def test => match elim Type {}
│ ╰────────────────╯
Error: Elimination match must be on variables
Parsing interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
MatchNumMismatch:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:1:12 ->
1 │ def test => match e as a, b returns Type {}
│ ╰─────────────────────────────╯
Error: I see 2 as-binding(s) but 1 discriminant(s)
Parsing interrupted due to:
1 error(s), 0 warning(s).
Let's learn from that.
ImplicitTuplePat:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:3 ->
1 │ def test (Sig Type ** Type) : Type
2 │ | ({a}, b) => a
│ ╰─╯
Error: Implicit pattern is not allowed here.
1 error(s), 0 warning(s).
Let's learn from that.
ImplicitListPat:
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:4:3 ->
2 │ open import arith::nat::base
3 │ def test (List Nat) : Nat
4 │ | [{a}] => a
│ ╰─╯
Error: Implicit elements in a list pattern is disallowed
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/data/list/base.aya:3:38 ->
1 │ open import arith::nat::base
2 │ open import relation::binary::path
3 │ open import data::maybe using (Maybe, Just, Nothing)
│ ╰──╯
Error: The qualified name `data::maybe::Just` is not defined in the current
scope
In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/data/list/base.aya:3:44 ->
1 │ open import arith::nat::base
2 │ open import relation::binary::path
3 │ open import data::maybe using (Maybe, Just, Nothing)
│ ╰─────╯
Error: The qualified name `data::maybe::Nothing` is not defined in the current
scope
Resolving interrupted due to:
3 error(s), 0 warning(s).
Let's learn from that.
>
|