Skip to content

Commit e1524dd

Browse files
committed
[ test ] Add test for #490
1 parent ae7b5f0 commit e1524dd

File tree

4 files changed

+20
-0
lines changed

4 files changed

+20
-0
lines changed
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
data MyList : Type -> Type where
2+
Nil : {a : Type} -> MyList a
3+
(::) : {a : Type} -> a -> MyList a -> MyList a
4+
5+
g : MyList a -> ()
6+
g [] = ()
7+
g l@(x :: xs) = ?hole
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
1/1: Building Issue490 (Issue490.idr)
2+
Main> a : Type
3+
x : a
4+
xs : MyList a
5+
l : MyList a
6+
------------------------------
7+
hole : ()
8+
Main>
9+
Bye for now!
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
:t hole

tests/idris2/linear/linear019/run

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
. ../../../testutils.sh
2+
3+
idris2 Issue490.idr < input

0 commit comments

Comments
 (0)