Update for totality warnings
Now, totality discrepancies prevent compilation. Add partial annotations
to totality005 to make it compile.
commit0cdef7fc1fe3c356030fe4a976ddf81da213e7af
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateTue 6 May 2014, 19:50 (12 years ago)
parenta6caf2d
test/totality005/expected−1
@@ -1,2 +1 @@
1−totality005.idr:6:1:Main.fib is possibly not total due to recursive path Main.fib
21[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 @@
22zipWithS : (f : a -> b -> c) -> Stream a -> Stream b -> Stream c
33zipWithS f (x :: xs) (y :: ys) = f x y :: zipWithS f xs ys
44
5+partial
56fib : Stream Nat
67fib = 0 :: zipWithS (+) fib (1 :: fib)
78
8−main : IO ()
9+partial main : IO ()
910main = print (take 15 fib)