git.iko.soy/Idris-dev
on master help sign in
Add regression test for #2349 (#4584)
1a7fa35Ryan Scott
test/TestData.hs+3−1
compare with master
unifiedsplit
@@ -182,7 +182,9 @@ testFamiliesData = [
182-- ( 5, ANY ),
182-- ( 5, ANY ),
183 ( 6, ANY ),
183 ( 6, ANY ),
184 ( 7, ANY ),
184 ( 7, ANY ),
185− ( 8, ANY )]),
185+ ( 8, ANY ),
186+-- ( 9, ANY ),
187+ ( 10, ANY )]),
186 ("interpret", "Interpret",
188 ("interpret", "Interpret",
187 [ ( 1, ANY ),
189 [ ( 1, ANY ),
188 ( 2, ANY ),
190 ( 2, ANY ),
test/interfaces010/expectednew file

No changes to the content.

test/interfaces010/interfaces010.idrnew file+12
@@ -0,0 +1,12 @@
1+module Test
2+
3+interface ListLike a where
4+ Elem : Type
5+ fromList : List Elem -> a
6+
7+data Silly = None | Cons Int Silly
8+
9+ListLike Silly where
10+ Elem = Int
11+ fromList [] = None
12+ fromList (x :: xs) = Cons x (fromList xs)
test/interfaces010/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces010.idr --check
3+rm -f interfaces010 *.ibc