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:34:6 -> 32 │ | _, [ ] => [ ] 33 │ | 0, _ :< _ => [ ] 34 │ | suc n, x :< xs => x :< (take n xs) │ ╰╯ Warning: The name `n` shadows a previous local definition from outer scope In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/data/list/base.aya:34:14 -> 32 │ | _, [ ] => [ ] 33 │ | 0, _ :< _ => [ ] 34 │ | suc n, x :< xs => x :< (take n xs) │ ╰╯ Warning: The name `xs` shadows a previous local definition from outer scope In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/data/list/base.aya:38:6 -> 36 │ def drop (n : Nat) (xs : List A) : List A 37 │ | 0, _ => xs 38 │ | suc n, [ ] => [ ] │ ╰╯ Warning: The name `n` shadows a previous local definition from outer scope In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/data/list/base.aya:39:6 -> 37 │ | 0, _ => xs 38 │ | suc n, [ ] => [ ] 39 │ | suc n, x :< xs => drop n xs │ ╰╯ Warning: The name `n` shadows a previous local definition from outer scope In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/shared/src/data/list/base.aya:39:14 -> 37 │ | 0, _ => xs 38 │ | suc n, [ ] => [ ] 39 │ | suc n, x :< xs => drop n xs │ ╰╯ Warning: The name `xs` shadows a previous local definition from outer scope 1 error(s), 5 warning(s). Let's learn from that. >