ac446bd · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -211,6 +211,9 @@ Extra-source-files:

211 test/reg033/run

212 test/reg033/*.idr

213 test/reg033/expected

214+ test/reg034/run

215+ test/reg034/*.idr

216+ test/reg034/expected

214

217

215 test/basic001/run

218 test/basic001/run

216 test/basic001/*.idr

219 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