Skip to content

Reduction Rule

Reduction Rule #94

Triggered via pull request December 12, 2023 23:40
@ice1000ice1000
synchronize #995
fn-shape
Status Success
Total duration 15s
Artifacts

commit-check.yaml

on: pull_request
commit-check
6s
commit-check
Fit to window
Zoom out
Zoom in

Annotations

4 errors
LibraryTest.fastTestOnDisk(): base/src/test/java/org/aya/test/LibraryTest.java#L53
org.opentest4j.AssertionFailedError: expected: <0> but was: <-1>
LibraryTest.[1] success: base/src/test/java/org/aya/test/LibraryTest.java#L44
org.opentest4j.AssertionFailedError: expected: <0> but was: <-1>
LibraryTest.testLiterate(): base/src/test/java/org/aya/test/LibraryTest.java#L64
org.opentest4j.AssertionFailedError: expected: <0> but was: <-1>
TestRunner.runAllAyaTests(): base/src/test/java/org/aya/test/TestRunner.java#L51
org.opentest4j.AssertionFailedError: issue354-confl.aya ==> expected: <In file /home/runner/work/aya-dev/aya-dev/base/src/test/resources/failure/patterns/issues/issue354-confl.aya:13:4 -> 11 │ { i := pos 0 | ~ i := neg 0 } 12 │ 13 │ def abs (n : Int) : Nat │ ╰─╯ 14 │ | pos n => suc n 15 │ | neg n => n 16 │ | posneg _ => 0 │ ╰───────────╯ (confluence check: this clause is substituted to) `0` Error: The 3rd clause matches on a constructor with condition(s). When checking the 1st condition, we failed to unify 0 for the arguments: posneg 1 Normalized: pos 0 suc 0 In particular, we failed to unify zero with suc 0 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/patterns/issues/issue354-confl.aya:13:4 -> 11 │ { i := pos 0 | ~ i := neg 0 } 12 │ 13 │ def abs (n : Int) : Nat │ ╰─╯ 14 │ | pos n => suc n 15 │ | neg n => n 16 │ | posneg _ => 0 │ ╰───────────╯ (confluence check: this clause is substituted to) `0` Error: The 3rd clause matches on a constructor with condition(s). When checking the 1st condition, we failed to unify 0 for the arguments: posneg 1 Normalized: pos 0 1 1 error(s), 0 warning(s). What are you doing? >