org.opentest4j.AssertionFailedError: tmp.aya ==> expected: <Unsolved: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:18 -> 1 │ open import arith::nat::base 2 │ def test : Nat => _ │ ╰╯ Error: Unsolved meta _ 1 error(s), 0 warning(s). Let's learn from that. Goal: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:28 -> 1 │ open import arith::nat::base 2 │ def test (a : Nat) : Nat => {? a ?} │ ╰─────╯ Goal: Goal of type Nat (Normalized: Nat) Context: a : Nat That looks right! UnsolvedMetaLit: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unsolved meta A in `Option ?A` in `Option ?A` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unsolved meta A in `some 114514` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unsolved meta A in `?A` in `114514` in `some 114514` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unsolved meta A in `114514` in `some 114514` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unable to solve the type of this literal: 114514 I'm confused about the following candidates: `Nat`, `Nat2` 5 error(s), 0 warning(s). Let's learn from that. Daylily: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:12 -> 3 │ def wow {A : Type 1} {B : A -> Type} (a b : A) (x : B a) (y : B b) : Bool => true 4 │ example def test1 (A B : Type) (x : A) (y : B) => 5 │ wow A B x y │ ╰╯ ╰╯ ?B A B x y A >= A │ ╰╯ ?B A B x y B >= B Info: Solving equation(s) with not very general solution(s) That looks right! Norell: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:28 -> 5 │ def test 6 │ (F : Type -> Type) 7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0 │ ╰╯ Error: Cannot check the expression X of type F (?_ F) against the type Type 0 In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:43 -> 5 │ def test 6 │ (F : Type -> Type) 7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0 │ ╰╯ Error: Cannot check the expression 0 of type Nat against the type F (?_ F) In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:41 -> 5 │ def test 6 │ (F : Type -> Type) 7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0 │ ╰─╯ Error: Cannot check the expression g 0 of type F (Neg <X>) (Normalized: F (<X> → Empty)) against the type Nat In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:15 -> 5 │ def test 6 │ (F : Type -> Type) 7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0 │ ╰╯ Error: Unsolved meta _ in `^0 (?_ ^0)` in `^0 (?_ ^0) → ^1 (Neg <X>)` 4 error(s), 0 warning(s). Let's learn from that. ScopeCheck: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 -> 3 │ 4 │ // https://cstheory.stackexchange.com/a/49160/50892 5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0 │ ╰╯ Error: The solution B is not well-scoped Only the variables below are allowed: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:41 -> 3 │ 4 │ // https://cstheory.stackexchange.com/a/49160/50892 5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0 │ ╰╯ │ ╰╯ ?_ <= ?A a B b Error: Equations do not have solutions! In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 -> 3 │ 4 │ // https://cstheory.stackexchange.com/a/49160/50892 5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0 │ ╰╯ Error: Unsolved meta _ 3 error(s), 0 warning(s). Let's learn from that. LiteralAmbiguous3: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:11 -> 4 │ 5 │ def good : List Unit => [ ] 6 │ def bad => [ unit ] │ ╰──────╯ Error: Unable to solve the type of this literal: [unit] I'm confused about the following candidates: `List`, `List2` 1 error(s), 0 warning(s). Let's learn from that. NonPattern: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:3 -> 6 │ def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A) 7 │ => Path (fn i => Vec (+-assoc i) A) 8 │ (xs ++ (ys ++ zs)) │ ╰──────────────╯ ?a n A m o xs ys zs 0 >= n, ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o 9 │ ((xs ++ ys) ++ zs) │ ╰──────────────╯ │ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m, ?c n A m o xs ys zs 1 >= o Info: Solving equation(s) with not very general solution(s) That looks right! UtensilFullFile: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:22 -> 7 │ def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A) 8 │ : Path (fn i ⇒ Vec (+-assoc i) A) 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs │ ╰──────────────╯ ╰──────────────╯ ?a n A m o xs ys zs 0 >= n, ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o │ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m, ?c n A m o xs ys zs 1 >= o Info: Solving equation(s) with not very general solution(s) In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ Error: The solution Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _ ys zs} i) (?A A x n m o _ ys zs) is not well-scoped Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`, `zs` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:25 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰─────────────╯ Error: Cannot check the expression ++-assoc' _ _ _ of type (++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs + ?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) ((++) {?m A x n m o _ ys zs} {?A A x n m o _ ys zs} {?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x n m o _ ys zs)) = (++) {?n A x n m o _ ys zs + ?m A x n m o _ ys zs} {?A A x n m o _ ys zs} {?o A x n m o _ ys zs} ((++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x n m o _ ys zs)) (?_ A x n m o _ ys zs) against the type ?a A x n m o _ ys zs = ?b A x n m o _ ys zs In particular, we failed to unify ?A A x n m o _ ys zs with Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _ ys zs} i) (?A A x n m o _ ys zs) In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ Error: The solution Vec (suc (+-assoc {n} {m} {o} i)) A is not well-scoped Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`, `zs` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:12 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰───────────────────────────╯ Error: Cannot check the expression pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _) of type (=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m o _ ys zs) (Normalized: (x :> ?a A x n m o _ ys zs) = (x :> ?b A x n m o _ ys zs)) against the type (++) {suc n} {A} {m + o} (x :> _) ((++) {m} {A} {o} ys zs) = (++) {suc n + m} {A} {o} ((++) {suc n} {A} {m} (x :> _) ys) zs (Normalized: (x :> (++) {n} {A} {m + o} _ ((++) {m} {A} {o} ys zs)) = (x :> (++) {n + m} {A} {o} ((++) {n} {A} {m} _ ys) zs)) In particular, we failed to unify ?B A x n m o _ ys zs with Vec (+-assoc {suc n} {m} {o} i) A (Normalized: Vec (suc (+-assoc {n} {m} {o} i)) A) In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ Error: The solution Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _) is not well-scoped Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`, `zs` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ Error: The solution Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _) is not well-scoped Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`, `zs` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ │ ╰──╯ ?B A x n m o _ ys zs >= Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _) │ ╰╯ ?A A x n m o _ ys zs <= Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _) Error: Equations do not have solutions! 7 error(s), 0 warning(s). Let's learn from that. > but was: <Unsolved: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:18 -> 1 │ open import arith::nat::base 2 │ def test : Nat => _ │ ╰╯ Error: Unsolved meta _ 1 error(s), 0 warning(s). Let's learn from that. Goal: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:2:28 -> 1 │ open import arith::nat::base 2 │ def test (a : Nat) : Nat => {? a ?} │ ╰─────╯ Goal: Goal of type Nat (Normalized: Nat) Context: a : Nat That looks right! UnsolvedMetaLit: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unsolved meta A in `Option ?A` in `Option ?A` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unsolved meta A in `some 114514` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unsolved meta A in `?A` in `114514` in `some 114514` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unsolved meta A in `114514` in `some 114514` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:17 -> 3 │ open inductive Option (A : Type) 4 │ | some A 5 │ def test => some 114514 │ ╰────╯ Error: Unable to solve the type of this literal: 114514 I'm confused about the following candidates: `Nat`, `Nat2` 5 error(s), 0 warning(s). Let's learn from that. Daylily: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:12 -> 3 │ def wow {A : Type 1} {B : A -> Type} (a b : A) (x : B a) (y : B b) : Bool => true 4 │ example def test1 (A B : Type) (x : A) (y : B) => 5 │ wow A B x y │ ╰╯ ╰╯ ?B A B x y A >= A │ ╰╯ ?B A B x y B >= B Info: Solving equation(s) with not very general solution(s) That looks right! Norell: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:28 -> 5 │ def test 6 │ (F : Type -> Type) 7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0 │ ╰╯ Error: Cannot check the expression X of type F (?_ F) against the type Type 0 In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:43 -> 5 │ def test 6 │ (F : Type -> Type) 7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0 │ ╰╯ Error: Cannot check the expression 0 of type Nat against the type F (?_ F) In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:41 -> 5 │ def test 6 │ (F : Type -> Type) 7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0 │ ╰─╯ Error: Cannot check the expression g 0 of type F (Neg <X>) (Normalized: F (<X> → Empty)) against the type Nat In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:7:15 -> 5 │ def test 6 │ (F : Type -> Type) 7 │ (g : ∀ (X : F _) -> F (Neg X)) : Nat => g 0 │ ╰╯ Error: Unsolved meta _ in `^0 (?_ ^0)` in `^0 (?_ ^0) → ^1 (Neg <X>)` 4 error(s), 0 warning(s). Let's learn from that. ScopeCheck: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 -> 3 │ 4 │ // https://cstheory.stackexchange.com/a/49160/50892 5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0 │ ╰╯ Error: The solution B is not well-scoped Only the variables below are allowed: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:41 -> 3 │ 4 │ // https://cstheory.stackexchange.com/a/49160/50892 5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0 │ ╰╯ │ ╰╯ ?_ <= ?A a B b Error: Equations do not have solutions! In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:5:14 -> 3 │ 4 │ // https://cstheory.stackexchange.com/a/49160/50892 5 │ def test (a : _) (B : Type) (b : B) (p : a = b) : I => 0 │ ╰╯ Error: Unsolved meta _ 3 error(s), 0 warning(s). Let's learn from that. LiteralAmbiguous3: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:4 -> 4 │ 5 │ def good : List Unit => [ ] 6 │ def bad => [ unit ] │ ╰─╯ Error: Unsolved meta _ In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:4 -> 4 │ 5 │ def good : List Unit => [ ] 6 │ def bad => [ unit ] │ ╰─╯ Error: Unsolved meta _ in `?_` in `[unit]` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:4 -> 4 │ 5 │ def good : List Unit => [ ] 6 │ def bad => [ unit ] │ ╰─╯ Error: Unsolved meta _ in `[unit]` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:6:11 -> 4 │ 5 │ def good : List Unit => [ ] 6 │ def bad => [ unit ] │ ╰──────╯ Error: Unable to solve the type of this literal: [unit] I'm confused about the following candidates: `List`, `List2` 4 error(s), 0 warning(s). Let's learn from that. NonPattern: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:3 -> 6 │ def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A) 7 │ => Path (fn i => Vec (+-assoc i) A) 8 │ (xs ++ (ys ++ zs)) │ ╰──────────────╯ ?a n A m o xs ys zs 0 >= n, ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o 9 │ ((xs ++ ys) ++ zs) │ ╰──────────────╯ │ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m, ?c n A m o xs ys zs 1 >= o Info: Solving equation(s) with not very general solution(s) That looks right! UtensilFullFile: In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:9:22 -> 7 │ def ++-assoc' (xs : Vec n A) (ys : Vec m A) (zs : Vec o A) 8 │ : Path (fn i ⇒ Vec (+-assoc i) A) 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs │ ╰──────────────╯ ╰──────────────╯ ?a n A m o xs ys zs 0 >= n, ?b n A m o xs ys zs 0 >= m, ?c n A m o xs ys zs 0 >= o │ ╰──────────────╯ ?a n A m o xs ys zs 1 >= n, ?b n A m o xs ys zs 1 >= m, ?c n A m o xs ys zs 1 >= o Info: Solving equation(s) with not very general solution(s) In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ Error: The solution Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _ ys zs} i) (?A A x n m o _ ys zs) is not well-scoped Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`, `zs` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:25 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰─────────────╯ Error: Cannot check the expression ++-assoc' _ _ _ of type (++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs + ?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) ((++) {?m A x n m o _ ys zs} {?A A x n m o _ ys zs} {?o A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x n m o _ ys zs)) = (++) {?n A x n m o _ ys zs + ?m A x n m o _ ys zs} {?A A x n m o _ ys zs} {?o A x n m o _ ys zs} ((++) {?n A x n m o _ ys zs} {?A A x n m o _ ys zs} {?m A x n m o _ ys zs} (?_ A x n m o _ ys zs) (?_ A x n m o _ ys zs)) (?_ A x n m o _ ys zs) against the type ?a A x n m o _ ys zs = ?b A x n m o _ ys zs In particular, we failed to unify ?A A x n m o _ ys zs with Vec (+-assoc {?n A x n m o _ ys zs} {?m A x n m o _ ys zs} {?o A x n m o _ ys zs} i) (?A A x n m o _ ys zs) In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ Error: The solution Vec (suc (+-assoc {n} {m} {o} i)) A is not well-scoped Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`, `zs` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:12 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰───────────────────────────╯ Error: Cannot check the expression pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _) of type (=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m o _ ys zs) (Normalized: (x :> ?a A x n m o _ ys zs) = (x :> ?b A x n m o _ ys zs)) against the type (++) {suc n} {A} {m + o} (x :> _) ((++) {m} {A} {o} ys zs) = (++) {suc n + m} {A} {o} ((++) {suc n} {A} {m} (x :> _) ys) zs (Normalized: (x :> (++) {n} {A} {m + o} _ ((++) {m} {A} {o} ys zs)) = (x :> (++) {n + m} {A} {o} ((++) {n} {A} {m} _ ys) zs)) In particular, we failed to unify ?B A x n m o _ ys zs with Vec (+-assoc {suc n} {m} {o} i) A (Normalized: Vec (suc (+-assoc {n} {m} {o} i)) A) In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ Error: The solution Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _) is not well-scoped Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`, `zs` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ Error: The solution Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _) is not well-scoped Only the variables below are allowed: `A`, `x`, `n`, `m`, `o`, `_`, `ys`, `zs` In file /home/runner/work/aya-dev/aya-dev/cli-impl/src/test/resources/tmp.aya:11:18 -> 9 │ (xs ++ (ys ++ zs)) ((xs ++ ys) ++ zs) elim xs 10 │ | [] ⇒ refl 11 │ | x :> _ => pmap (x :>) (++-assoc' _ _ _) │ ╰──╯ │ ╰──╯ ?B A x n m o _ ys zs >= Vec (suc (?n A x n m o _ ys zs _)) (?A A x n m o _ ys zs _) │ ╰╯ ?A A x n m o _ ys zs <= Vec (?n A x n m o _ ys zs _) (?A A x n m o _ ys zs _) Error: Equations do not have solutions! 7 error(s), 0 warning(s). Let's learn from that. >