git.iko.soy/Idris-dev

on master help sign in

test/proof007/expected+1−1

compare with master

unifiedsplit

@@ -1,4 +1,4 @@

1DefaultArgUnknownName.idr:9:6:

1DefaultArgUnknownName.idr:9:6:

2When elaborating right hand side of test:

2When elaborating right hand side of test:

3−When elaborating argument arg to function DefaultArgUnknownName.funWithBadDefArg:

3+When elaborating argument arg to function DefaultArgUnknownName.funWithBadDefArg:

4 No such variable sadgjhsag

4 No such variable sadgjhsag

test/proof007/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 --check $@ DefaultArgUnknownName.idr

2+idris --nocolour --consolewidth 80 --check $@ DefaultArgUnknownName.idr

3rm -f *.ibc

3rm -f *.ibc

test/reg023/expected+2−2

@@ -1,5 +1,5 @@

1reg023.idr:7:5:When elaborating right hand side of bad:

1reg023.idr:7:5:When elaborating right hand side of bad:

2Can't unify

2Can't unify

3− Nat (Type of 0)

3+ Nat (Type of 0)

4with

4with

5− f Nat (Expected type)

5+ f Nat (Expected type)

test/reg023/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ reg023.idr --check

2+idris --nocolour --consolewidth 80 $@ reg023.idr --check

3rm -f *.ibc

3rm -f *.ibc

test/reg034/expected+2−2

@@ -1,4 +1,4 @@

1reg034.idr:6:5:When elaborating left hand side of bar:

1reg034.idr:6:5:When elaborating left hand side of bar:

2−Can't match on bar xs xs Refl

2+Can't match on bar xs xs Refl

3reg034.idr:9:5:When elaborating left hand side of foo:

3reg034.idr:9:5:When elaborating left hand side of foo:

4−Can't match on foo f x x Refl

4+Can't match on foo f x x Refl

test/reg034/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 --check reg034.idr

2+idris --nocolour --consolewidth 80 --check reg034.idr

3rm -f reg034 *.ibc

3rm -f reg034 *.ibc

test/reg035/expected+2−2

@@ -1,4 +1,4 @@

1reg035b.idr:8:6:Can't convert

1reg035b.idr:8:6:Can't convert

2− Additive -> Nat

2+ Additive -> Nat

3with

3with

4− Fin 0

4+ Fin 0

test/reg035/run+3−3

@@ -1,5 +1,5 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 --check reg035.idr

2+idris --nocolour --consolewidth 80 --check reg035.idr

3−idris --consolewidth 80 --check reg035a.lidr

3+idris --nocolour --consolewidth 80 --check reg035a.lidr

4−idris --consolewidth 80 --check reg035b.idr

4+idris --nocolour --consolewidth 80 --check reg035b.idr

5rm -f *.ibc

5rm -f *.ibc

test/reg044/expected+4−4

@@ -1,11 +1,11 @@

1reg044.idr:4:4:When elaborating right hand side of Main.pf:

1reg044.idr:4:4:When elaborating right hand side of Main.pf:

2Can't unify

2Can't unify

3− b = b (Type of Refl)

3+ b = b (Type of Refl)

4with

4with

5− a = b (Expected type)

5+ a = b (Expected type)

6

6

7Specifically:

7Specifically:

8 Can't unify

8 Can't unify

9− b

9+ b

10 with

10 with

11− a

11+ a

test/reg044/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 reg044.idr --check

2+idris --nocolour --consolewidth 80 reg044.idr --check

3rm -f *.ibc

3rm -f *.ibc

test/reg054/expected+4−4

@@ -1,10 +1,10 @@

1reg054.idr:18:5:When elaborating left hand side of inf:

1reg054.idr:18:5:When elaborating left hand side of inf:

2−When elaborating an application of constructor Main.MkInfer:

2+When elaborating an application of constructor Main.MkInfer:

3 Attempting concrete match on polymorphic argument: 0

3 Attempting concrete match on polymorphic argument: 0

4reg054.idr:34:7:When elaborating left hand side of weird:

4reg054.idr:34:7:When elaborating left hand side of weird:

5−When elaborating argument x to Main.weird:

5+When elaborating argument x to Main.weird:

6 No explicit types on left hand side: Char

6 No explicit types on left hand side: Char

7reg054.idr:37:9:Can't convert

7reg054.idr:37:9:Can't convert

8− Maybe a1

8+ Maybe a1

9with

9with

10− a

10+ a

test/reg054/run+1−1

@@ -1,2 +1,2 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ reg054.idr --check

2+idris --nocolour --consolewidth 80 $@ reg054.idr --check

test/reg055/expected+3−3

@@ -1,9 +1,9 @@

1reg055.idr:5:3:When elaborating left hand side of g:

1reg055.idr:5:3:When elaborating left hand side of g:

2−Can't match on g (f 0)

2+Can't match on g (f 0)

3reg055.idr:8:3:When elaborating left hand side of h:

3reg055.idr:8:3:When elaborating left hand side of h:

4Can't match on h x x

4Can't match on h x x

5reg055a.idr:8:5:When elaborating left hand side of foo:

5reg055a.idr:8:5:When elaborating left hand side of foo:

6−When elaborating an application of constructor Foo.CAny:

6+When elaborating an application of constructor Foo.CAny:

7 Attempting concrete match on polymorphic argument: Nothing

7 Attempting concrete match on polymorphic argument: Nothing

8reg055a.idr:13:7:When elaborating left hand side of Foo.apply:

8reg055a.idr:13:7:When elaborating left hand side of Foo.apply:

9−Can't match on apply (\x => \y => x) a

9+Can't match on apply (\x => \y => x) a

test/reg055/run+2−2

@@ -1,5 +1,5 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ reg055.idr --check

2+idris --nocolour --consolewidth 80 $@ reg055.idr --check

3−idris --consolewidth 80 $@ reg055a.idr --check

3+idris --nocolour --consolewidth 80 $@ reg055a.idr --check

4rm -f *.ibc

4rm -f *.ibc

5

5

test/tutorial006/expected+9−9

@@ -1,24 +1,24 @@

1tutorial006a.idr:5:23:When elaborating right hand side of vapp:

1tutorial006a.idr:5:23:When elaborating right hand side of vapp:

2−When elaborating argument xs to constructor Data.VectType.Vect.:::

2+When elaborating argument xs to constructor Data.VectType.Vect.:::

3 Can't unify

3 Can't unify

4− Vect (n + n) a (Type of vapp xs xs)

4+ Vect (n + n) a (Type of vapp xs xs)

5 with

5 with

6− Vect (plus n m) a (Expected type)

6+ Vect (plus n m) a (Expected type)

7

7

8 Specifically:

8 Specifically:

9 Can't unify

9 Can't unify

10− plus n n

10+ plus n n

11 with

11 with

12− plus n m

12+ plus n m

13tutorial006b.idr:10:10:

13tutorial006b.idr:10:10:

14When elaborating right hand side of with block in Main.parity:

14When elaborating right hand side of with block in Main.parity:

15Can't unify

15Can't unify

16− Parity (plus (S j) (S j)) (Type of even)

16+ Parity (plus (S j) (S j)) (Type of even)

17with

17with

18− Parity (S (S (plus j j))) (Expected type)

18+ Parity (S (S (plus j j))) (Expected type)

19

19

20Specifically:

20Specifically:

21 Can't unify

21 Can't unify

22− plus (S j) (S j)

22+ plus (S j) (S j)

23 with

23 with

24− S (S (plus j j))

24+ S (S (plus j j))

test/tutorial006/run+2−2

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ tutorial006a.idr --check

2+idris --nocolour --consolewidth 80 $@ tutorial006a.idr --check

3−idris --consolewidth 80 $@ tutorial006b.idr --check

3+idris --nocolour --consolewidth 80 $@ tutorial006b.idr --check

4rm -f *.ibc

4rm -f *.ibc

test/unique001/expected+6−6

@@ -3,17 +3,17 @@

338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

338,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

438,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

438,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

5unique001a.idr:33:11:Can't convert

5unique001a.idr:33:11:Can't convert

6− Int -> String

6+ Int -> String

7with

7with

8− UniqueType (Int -> String)

8+ UniqueType (Int -> String)

9unique001a.idr:44:12:Can't convert

9unique001a.idr:44:12:Can't convert

10− Int -> String

10+ Int -> String

11with

11with

12− UniqueType (Int -> String)

12+ UniqueType (Int -> String)

13unique001a.idr:55:12:Can't convert

13unique001a.idr:55:12:Can't convert

14− UniqueType (Int -> String)

14+ UniqueType (Int -> String)

15with

15with

16− Int -> String

16+ Int -> String

17unique001b.idr:16:7:Borrowed name xs must not be used on RHS

17unique001b.idr:16:7:Borrowed name xs must not be used on RHS

18unique001c.idr:46:6:Unique name f is used more than once

18unique001c.idr:46:6:Unique name f is used more than once

19unique001d.idr:3:7:Borrowed name x must not be used on RHS

19unique001d.idr:3:7:Borrowed name x must not be used on RHS

test/unique001/run+6−6

@@ -1,9 +1,9 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ unique001.idr -o unique001

2+idris --nocolour --consolewidth 80 $@ unique001.idr -o unique001

3./unique001

3./unique001

4−idris --consolewidth 80 $@ unique001a.idr --check

4+idris --nocolour --consolewidth 80 $@ unique001a.idr --check

5−idris --consolewidth 80 $@ unique001b.idr --check

5+idris --nocolour --consolewidth 80 $@ unique001b.idr --check

6−idris --consolewidth 80 $@ unique001c.idr --check

6+idris --nocolour --consolewidth 80 $@ unique001c.idr --check

7−idris --consolewidth 80 $@ unique001d.idr --check

7+idris --nocolour --consolewidth 80 $@ unique001d.idr --check

8−idris --consolewidth 80 $@ unique001e.idr --check

8+idris --nocolour --consolewidth 80 $@ unique001e.idr --check

9rm -f unique001 *.ibc

9rm -f unique001 *.ibc

test/unique002/expected+2−2

@@ -1,5 +1,5 @@

1unique002.idr:15:5:Unique name xs is used more than once

1unique002.idr:15:5:Unique name xs is used more than once

2unique002a.idr:15:5:Can't convert

2unique002a.idr:15:5:Can't convert

3− Int -> String

3+ Int -> String

4with

4with

5− UniqueType (Int -> String)

5+ UniqueType (Int -> String)

test/unique002/run+2−2

@@ -1,4 +1,4 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ unique002.idr --check

2+idris --nocolour --consolewidth 80 $@ unique002.idr --check

3−idris --consolewidth 80 $@ unique002a.idr --check

3+idris --nocolour --consolewidth 80 $@ unique002a.idr --check

4rm -f *.ibc

4rm -f *.ibc

test/unique003/expected+2−2

@@ -1,4 +1,4 @@

1unique003.idr:18:5:Can't convert

1unique003.idr:18:5:Can't convert

2− Int -> String

2+ Int -> String

3with

3with

4− UniqueType (Int -> String)

4+ UniqueType (Int -> String)

test/unique003/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

1#!/usr/bin/env bash

2−idris --consolewidth 80 $@ unique003.idr --check

2+idris --nocolour --consolewidth 80 $@ unique003.idr --check

3rm -f *.ibc

3rm -f *.ibc