Skip to content

Commit

Permalink
fix: what did I just push??
Browse files Browse the repository at this point in the history
  • Loading branch information
HoshinoTented committed Dec 29, 2024
1 parent 6253f37 commit 5634d92
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 19 deletions.
9 changes: 0 additions & 9 deletions cli-impl/src/test/resources/negative/GoalAndMeta.txt
Original file line number Diff line number Diff line change
Expand Up @@ -190,15 +190,6 @@ Error: Unable to solve the type of this literal:
Let's learn from that.

NonPattern:
In file C:\Users\hoshino\Documents\Projects\project-aya\aya-dev\cli-impl\src\test\resources\shared\src\data\vec\base.aya:5:6 ->

3 │ open inductive Vec (n : Nat) (A : Type) elim n
4 │ | 0 => []
5 │ | suc n => infixr :> A (Vec n A)
│ ╰╯

Warning: The name `n` shadows a previous local definition from outer scope

In file $FILE:9:3 ->

6 │ def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
Expand Down
11 changes: 1 addition & 10 deletions cli-impl/src/test/resources/negative/PatTyckError.txt
Original file line number Diff line number Diff line change
Expand Up @@ -13,15 +13,6 @@ Error: Unknown constructor
Let's learn from that.

SelectionFailed:
In file C:\Users\hoshino\Documents\Projects\project-aya\aya-dev\cli-impl\src\test\resources\shared\src\data\vec\base.aya:5:6 ->

3 │ open inductive Vec (n : Nat) (A : Type) elim n
4 │ | 0 => []
5 │ | suc n => infixr :> A (Vec n A)
│ ╰╯

Warning: The name `n` shadows a previous local definition from outer scope

In file $FILE:4:2 ->

2 │ open import data::vec::base
Expand All @@ -46,7 +37,7 @@ Error: I'm unsure if there should be a case for
as index unification is blocked for type
Vec (<n> + <n>) A

2 error(s), 1 warning(s).
2 error(s), 0 warning(s).
Let's learn from that.

SelectionBlocked:
Expand Down

0 comments on commit 5634d92

Please sign in to comment.