d9b8bcb · Idris-dev · git.iko.soy

test/reg044/expecteddeleted−15

compare with master

unifiedsplit

@@ -1,15 +0,0 @@

1−reg044.idr:4:6-11:

2−This style of tactic proof is deprecated. See %runElab for the replacement.

3−reg044.idr:4:4:When checking right hand side of Main.pf with expected type

4− (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

5−

6−Type mismatch between

7− b = b (Type of Refl)

8−and

9− a = b (Expected type)

10−

11−Specifically:

12− Type mismatch between

13− b

14− and

15− a

test/reg044/rundeleted−3

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

1−#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --nocolour reg044.idr --check

3−rm -f *.ibc

test/regression002/expected+16

@@ -52,3 +52,19 @@ Can't match on bar xs xs Refl

52reg034.idr:9:5:When checking left hand side of foo:

53Can't match on foo f x x Refl

54reg035b.idr:8:6:No such variable __pi_arg

55+reg044.idr:4:6-11:

56+This style of tactic proof is deprecated. See %runElab for the replacement.

57+reg044.idr:4:4:

58+When checking right hand side of Main.pf with expected type

59+ (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b

60+

61+Type mismatch between

62+ b = b (Type of Refl)

63+and

64+ a = b (Expected type)

65+

66+Specifically:

67+ Type mismatch between

68+ b

69+ and

70+ a

test/reg044/reg044.idr → test/regression002/reg044.idrrenamed

The content is the same.

test/regression002/run+1

@@ -17,6 +17,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!

17:load reg035.idr

18:load reg035a.lidr

19:load reg035b.idr

20+:load reg044.idr

20!

21!

21

22

22rm -f *.ibc

23rm -f *.ibc