Let Term #2717
HoshinoTentedAnnotations
5 errors and 1 warning
|
LibraryTest.fastTestOnDisk():
base/src/test/java/org/aya/test/LibraryTest.java#L53
java.lang.AssertionError: Failed with `class org.aya.tyck.error.UnifyError$Type`: In file TypeTheory/Thorsten.aya:56:39 ->
54 | | _, Subst B δ => π₂β {Δ : Con} (t : Tm Γ A)
55 | : transport (Tm _) (pmap (Subst B) (π₁β t)) (π₂ (δ ∷ t)) = t
56 | | _ ▷ _, A => Πβ (f : Tm Γ A) : app (λ f) = f
| ^^
Error: Cannot check the expression
f
of type
Tm Γ A
against the type
Tm (Γ ▷ A') B'
(Normalized: Tm (Γ ▷ _) A)
In particular, we failed to unify
_
with
_ ▷ _
at (1930-1930) [56,39-56,39]
|
|
LibraryTest.testInMemoryAndPrim():
base/src/test/java/org/aya/test/LibraryTest.java#L78
java.lang.AssertionError: Failed with `class org.aya.tyck.error.UnifyError$Type`: In file TypeTheory/Thorsten.aya:56:39 ->
54 | | _, Subst B δ => π₂β {Δ : Con} (t : Tm Γ A)
55 | : transport (Tm _) (pmap (Subst B) (π₁β t)) (π₂ (δ ∷ t)) = t
56 | | _ ▷ _, A => Πβ (f : Tm Γ A) : app (λ f) = f
| ^^
Error: Cannot check the expression
f
of type
Tm Γ A
against the type
Tm (Γ ▷ A') B'
(Normalized: Tm (Γ ▷ _) A)
In particular, we failed to unify
_
with
_ ▷ _
at (1930-1930) [56,39-56,39]
|
|
LibraryTest.[1] success:
base/src/test/java/org/aya/test/LibraryTest.java#L44
java.lang.AssertionError: Failed with `class org.aya.tyck.error.UnifyError$Type`: In file TypeTheory/Thorsten.aya:56:39 ->
54 | | _, Subst B δ => π₂β {Δ : Con} (t : Tm Γ A)
55 | : transport (Tm _) (pmap (Subst B) (π₁β t)) (π₂ (δ ∷ t)) = t
56 | | _ ▷ _, A => Πβ (f : Tm Γ A) : app (λ f) = f
| ^^
Error: Cannot check the expression
f
of type
Tm Γ A
against the type
Tm (Γ ▷ A') B'
(Normalized: Tm (Γ ▷ _) A)
In particular, we failed to unify
_
with
_ ▷ _
at (1930-1930) [56,39-56,39]
|
|
LibraryTest.testLiterate():
base/src/test/java/org/aya/test/LibraryTest.java#L64
java.lang.AssertionError: Failed with `class org.aya.tyck.error.UnifyError$Type`: In file TypeTheory/Thorsten.aya:56:39 ->
54 | | _, Subst B δ => π₂β {Δ : Con} (t : Tm Γ A)
55 | : transport (Tm _) (pmap (Subst B) (π₁β t)) (π₂ (δ ∷ t)) = t
56 | | _ ▷ _, A => Πβ (f : Tm Γ A) : app (λ f) = f
| ^^
Error: Cannot check the expression
f
of type
Tm Γ A
against the type
Tm (Γ ▷ A') B'
(Normalized: Tm (Γ ▷ _) A)
In particular, we failed to unify
_
with
_ ▷ _
at (1930-1930) [56,39-56,39]
|
|
TestRunner.runAllAyaTests():
base/src/test/java/org/aya/test/TestRunner.java#L50
org.opentest4j.AssertionFailedError: no-more-var.aya ==> expected: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/holes/no-more-var.aya:4:7 ->
2 │
3 │ def justMatch {n : Nat} (m : Nat) : Nat
4 │ | m => {??}
│ ╰──╯
Goal: Goal of type
Nat
(Normalized: Nat)
Context:
{m : Nat}
{n : Nat} (not in scope)
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/holes/no-more-var.aya:4:7 ->
2 │
3 │ def justMatch {n : Nat} (m : Nat) : Nat
4 │ | m => {??}
│ ╰──╯
Error: Unsolved meta _
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/holes/no-more-var.aya:4:7 ->
2 │
3 │ def justMatch {n : Nat} (m : Nat) : Nat
4 │ | m => {??}
│ ╰──╯
Goal: Goal of type
Nat
(Normalized: Nat)
Context:
{m : Nat} (not in scope)
{n : Nat}
{m : Nat}
{n : Nat} (not in scope)
In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/holes/no-more-var.aya:4:7 ->
2 │
3 │ def justMatch {n : Nat} (m : Nat) : Nat
4 │ | m => {??}
│ ╰──╯
Error: Unsolved meta _
1 error(s), 0 warning(s).
What are you doing?
>
|
|
commit-check
Node.js 12 actions are deprecated. Please update the following actions to use Node.js 16: actions/checkout@v2. For more information see: https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/.
|