org.opentest4j.AssertionFailedError: expected: <true> but was: <false>

org.opentest4j.AssertionFailedError: expected: <true> but was: <false>

org.opentest4j.AssertionFailedError: expected: <suc zero :< nil> but was: <1 :< nil>

org.aya.util.error.InternalException: class org.aya.core.term.ShapedFnCall: suc (a + b)

org.aya.util.error.InternalException: class org.aya.core.term.ShapedFnCall: suc a

java.lang.AssertionError: Failed with `class org.aya.terck.BadRecursion`: In file Assoc.aya:40:4 -> 38 | tighter = ==< qed 39 | 40 | def +'-comm (a b : Nat) : a +' b = b +' a | ^-----^ Error: The recursive definition `+'-comm` is not structurally recursive note: In particular, the problematic call is: +'-comm (suc a) b whose call matrix is: ? ? ? ? whose diagonal is: ? ? at (936-942) [40,4-40,10]

java.lang.AssertionError: Failed with `class org.aya.terck.BadRecursion`: In file Assoc.aya:40:4 -> 38 | tighter = ==< qed 39 | 40 | def +'-comm (a b : Nat) : a +' b = b +' a | ^-----^ Error: The recursive definition `+'-comm` is not structurally recursive note: In particular, the problematic call is: +'-comm (suc a) b whose call matrix is: ? ? ? ? whose diagonal is: ? ? at (936-942) [40,4-40,10]

java.lang.AssertionError: Failed with `class org.aya.terck.BadRecursion`: In file Assoc.aya:40:4 -> 38 | tighter = ==< qed 39 | 40 | def +'-comm (a b : Nat) : a +' b = b +' a | ^-----^ Error: The recursive definition `+'-comm` is not structurally recursive note: In particular, the problematic call is: +'-comm (suc a) b whose call matrix is: ? ? ? ? whose diagonal is: ? ? at (936-942) [40,4-40,10]

java.lang.AssertionError: Failed with `class org.aya.terck.BadRecursion`: In file Assoc.aya:40:4 -> 38 | tighter = ==< qed 39 | 40 | def +'-comm (a b : Nat) : a +' b = b +' a | ^-----^ Error: The recursive definition `+'-comm` is not structurally recursive note: In particular, the problematic call is: +'-comm (suc a) b whose call matrix is: ? ? ? ? whose diagonal is: ? ? at (936-942) [40,4-40,10]

org.opentest4j.AssertionFailedError: confl-literal.aya ==> expected: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 -> 1 │ open data Nat | zero | suc Nat 2 │ 3 │ overlap def test Nat : Nat │ ╰──╯ 4 │ | 0 => 0 5 │ | a => a │ ╰────╯ (confluence check: this clause is substituted to) `114514` 6 │ | suc a => suc a 7 │ | suc (suc a) => a 8 │ | 2147483647 => 3 9 │ | 2147483647 => 4 10 │ | 114514 => 1919 │ ╰────────────╯ (confluence check: this clause is substituted to) `1919` Error: The 2nd and the 7th clauses are not confluent because we failed to unify 1919 and 114514 In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 -> 1 │ open data Nat | zero | suc Nat 2 │ 3 │ overlap def test Nat : Nat │ ╰──╯ 4 │ | 0 => 0 5 │ | a => a 6 │ | suc a => suc a │ ╰────────────╯ (confluence check: this clause is substituted to) `suc (suc a)` 7 │ | suc (suc a) => a │ ╰──────────────╯ (confluence check: this clause is substituted to) `a` Error: The 4th and the 3rd clauses are not confluent because we failed to unify suc (suc a) and a In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 -> 1 │ open data Nat | zero | suc Nat 2 │ 3 │ overlap def test Nat : Nat │ ╰──╯ 4 │ | 0 => 0 5 │ | a => a 6 │ | suc a => suc a 7 │ | suc (suc a) => a 8 │ | 2147483647 => 3 │ ╰─────────────╯ (confluence check: this clause is substituted to) `3` 9 │ | 2147483647 => 4 │ ╰─────────────╯ (confluence check: this clause is substituted to) `4` Error: The 6th and the 5th clauses are not confluent because we failed to unify 3 and 4 In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 -> 1 │ open data Nat | zero | suc Nat 2 │ 3 │ overlap def test Nat : Nat │ ╰──╯ 4 │ | 0 => 0 5 │ | a => a │ ╰────╯ (confluence check: this clause is substituted to) `2147483647` 6 │ | suc a => suc a 7 │ | suc (suc a) => a 8 │ | 2147483647 => 3 9 │ | 2147483647 => 4 │ ╰─────────────╯ (confluence check: this clause is substituted to) `4` Error: The 2nd and the 6th clauses are not confluent because we failed to unify 4 and 2147483647 In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 -> 1 │ open data Nat | zero | suc Nat 2 │ 3 │ overlap def test Nat : Nat │ ╰──╯ 4 │ | 0 => 0 5 │ | a => a 6 │ | suc a => suc a │ ╰────────────╯ (confluence check: this clause is substituted to) `suc (suc a)` 7 │ | suc (suc a) => a │ ╰──────────────╯ (confluence check: this clause is substituted to) `a` Error: The 4th and the 3rd clauses are not confluent because we failed to unify suc (suc a) and a In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 -> 1 │ open data Nat | zero | suc Nat 2 │ 3 │ overlap def test Nat : Nat │ ╰──╯ 4 │ | 0 => 0 5 │ | a => a 6 │ | suc a => suc a │ ╰────────────╯ (confluence check: this clause is substituted to) `suc (suc a)` 7 │ | suc (suc a) => a │ ╰──────────────╯ (confluence check: this clause is substituted to) `a` Error: The 4th and the 3rd clauses are not confluent because we failed to unify suc (suc a) and a In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:4:4 -> 2 │ 3 │ overlap def test Nat : Nat 4 │ | 0 => 0 │ ╰────╯ Warning: The 2nd clause dominates the 1st clause. The 1st clause will be unreachable In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:6:4 -> 4 │ | 0 => 0 5 │ | a => a 6 │ | suc a => suc a │ ╰────────────╯ Warning: The 2nd clause dominates the 3rd clause. The 3rd clause will be unreachable In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:10:4 -> 8 │ | 2147483647 => 3 9 │ | 2147483647 => 4 10 │ | 114514 => 1919 │ ╰────────────╯ Warning: The 2nd clause dominates the 7th clause. The 7th clause will be unreachable In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:7:4 -> 5 │ | a => a 6 │ | suc a => suc a 7 │ | suc (suc a) => a │ ╰──────────────╯ Warning: The 3rd clause dominates the 4th clause. The 4th clause will be unreachable In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:9:4 -> 7 │ | suc (suc a) => a 8 │ | 2147483647 => 3 9 │ | 2147483647 => 4 │ ╰─────────────╯ Warning: The 5th clause dominates the 6th clause. The 6th clause will be unreachable In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:8:4 -> 6 │ | suc a => suc a 7 │ | suc (suc a) => a 8 │ | 2147483647 => 3 │ ╰─────────────╯ Warning: The 6th clause dominates the 5th clause. The 5th clause will be unreachable In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:9:4 -> 7 │ | suc (suc a) => a 8 │ | 2147483647 => 3 9 │ | 2147483647 => 4 │ ╰─────────────╯ Warning: The 2nd clause dominates the 6th clause. The 6th clause will be unreachable 6 error(s), 7 warning(s). What are you doing? > but was: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/confl-literal.aya:3:12 -> 1 │ open data Nat | zero | suc Nat 2 │ 3 │ overlap def test Nat : Nat │ ╰──╯ 4 │ | 0 => 0 5 │ | a => a │ ╰────╯ (confluence check: this clause is substituted to) `114514` 6 │ | suc a => suc a 7 │ | suc (suc a) => a 8 │ | 2147483647 => 3 9 │ | 2147483647 => 4 10 │ | 114514 => 1919 │ ╰────────────╯ (confluence check: this clause is substituted to) `1919` Error: The 2nd and the 7th clauses are not confluent because we failed to unify 1919 and 114514 Internal error >