git.iko.soy/Idris-dev
on master help sign in
Update for totality warnings
0cdef7fDavid Raymond Christiansen
test/totality005/expected−1
compare with master
unifiedsplit
@@ -1,2 +1 @@
1−totality005.idr:6:1:Main.fib is possibly not total due to recursive path Main.fib
2[0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377]
1[0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377]
test/totality005/totality005.idr+2−1
@@ -2,8 +2,9 @@
2zipWithS : (f : a -> b -> c) -> Stream a -> Stream b -> Stream c
2zipWithS : (f : a -> b -> c) -> Stream a -> Stream b -> Stream c
3zipWithS f (x :: xs) (y :: ys) = f x y :: zipWithS f xs ys
3zipWithS f (x :: xs) (y :: ys) = f x y :: zipWithS f xs ys
4
4
5+partial
5fib : Stream Nat
6fib : Stream Nat
6fib = 0 :: zipWithS (+) fib (1 :: fib)
7fib = 0 :: zipWithS (+) fib (1 :: fib)
7
8
8−main : IO ()
9+partial main : IO ()
9main = print (take 15 fib)
10main = print (take 15 fib)