git.iko.soy/Idris-dev
on master help sign in
Updated test
6e5ee86Edwin Brady
test/reg018/expected+2
compare with master
unifiedsplit
@@ -4,6 +4,8 @@ reg018a.idr:21:1:
4conat.loopForever is possibly not total due to: conat.minusCoNat
4conat.loopForever is possibly not total due to: conat.minusCoNat
5reg018b.idr:8:1:
5reg018b.idr:8:1:
6A.showB is possibly not total due to recursive path A.showB
6A.showB is possibly not total due to recursive path A.showB
7+reg018b.idr:11:1:
8+A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
7reg018c.idr:21:1:
9reg018c.idr:21:1:
8CodataTest.inf is possibly not total due to: with block in CodataTest.inf
10CodataTest.inf is possibly not total due to: with block in CodataTest.inf
9reg018d.idr:8:1:
11reg018d.idr:8:1:
test/reg018/reg018b.idr+1−1
@@ -8,7 +8,7 @@ showB : B -> String
8showB (I x) = "I" ++ showB x
8showB (I x) = "I" ++ showB x
9showB (Z x) = "Z" ++ showB x
9showB (Z x) = "Z" ++ showB x
10
10
11−implementation Show B where show = showB
11+Show B where show = showB
12
12
13os : B
13os : B
14os = Z os
14os = Z os