Add new regression test
commitac446bd5665203d9b59c82b018da98e78799bf33
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 17 Feb 2014, 02:08 (13 years ago)
parent2cff556
idris.cabal+3
@@ -211,6 +211,9 @@ Extra-source-files:
211211 test/reg033/run
212212 test/reg033/*.idr
213213 test/reg033/expected
214+ test/reg034/run
215+ test/reg034/*.idr
216+ test/reg034/expected
214217
215218 test/basic001/run
216219 test/basic001/*.idr
test/reg034/expectednew file+22
@@ -0,0 +1,22 @@
1+reg034.idr:6:5:When elaborating left hand side of bar:
2+Can't unify
3+ [92mlength[0m [95mys[0m [94m=[0m [92mlength[0m [95mys[0m
4+with
5+ [92mlength[0m [95mxs[0m [94m=[0m [92mlength[0m [95mys[0m
6+
7+Specifically:
8+ Can't unify
9+ [92mlength[0m [95mys[0m
10+ with
11+ [92mlength[0m [95mxs[0m
12+reg034.idr:9:5:When elaborating left hand side of foo:
13+Can't unify
14+ [95mf[0m [95my[0m [94m=[0m [95mf[0m [95my[0m
15+with
16+ [95mf[0m [95mx[0m [94m=[0m [95mf[0m [95my[0m
17+
18+Specifically:
19+ Can't unify
20+ [95mf[0m [95my[0m
21+ with
22+ [95mf[0m [95mx[0m
test/reg034/reg034.idrnew file+10
@@ -0,0 +1,10 @@
1+module main
2+import Prelude.List
3+
4+bar : (xs : List ()) -> (ys : List ()) ->
5+ Prelude.List.length xs = Prelude.List.length ys -> xs = ys
6+bar xs xs refl = refl
7+
8+foo : (f : Nat -> Nat) -> (x : Nat) -> (y : Nat) -> f x = f y -> x = y
9+foo f x x refl = refl
10+
test/reg034/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris --check reg034.idr
3+rm -f reg034 *.ibc