Skip to content

Commit feb1bc9

Browse files
committed
[ test ] Add test for idris-lang#2159
1 parent 297e757 commit feb1bc9

File tree

3 files changed

+23
-0
lines changed

3 files changed

+23
-0
lines changed
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
plusRRNever1 : {r:Nat} -> plus r r = 1 -> Void
2+
plusRRNever1 {r = 0} Refl impossible
3+
plusRRNever1 {r = (S 0)} Refl impossible
4+
plusRRNever1 {r = (S (S k))} prf = ?somethingWrong
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
1/1: Building Issue2159 (Issue2159.idr)
2+
Warning: Issue2159:2:19--2:20:Can't deal with fromInteger in impossible clauses yet
3+
4+
Issue2159:2:19--2:20
5+
1 | plusRRNever1 : {r:Nat} -> plus r r = 1 -> Void
6+
2 | plusRRNever1 {r = 0} Refl impossible
7+
^
8+
9+
Warning: Issue2159:3:22--3:23:Can't deal with fromInteger in impossible clauses yet
10+
11+
Issue2159:3:22--3:23
12+
1 | plusRRNever1 : {r:Nat} -> plus r r = 1 -> Void
13+
2 | plusRRNever1 {r = 0} Refl impossible
14+
3 | plusRRNever1 {r = (S 0)} Refl impossible
15+
^
16+
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
. ../../../testutils.sh
2+
3+
check Issue2159.idr

0 commit comments

Comments
 (0)