Dabbling into Idris, I was trying to port this Haskell function to Idris. I think I succeeded, with this code...
windowl : Nat -> List a -> List (List a)
windowl size = loop
where
loop xs = case List.splitAt size xs of
(ys, []) => if length ys == size then [ys] else []
(ys, _) => ys :: loop (drop 1 xs)
However, when I call it in interactive idris, it appears that only the first call into the function is evaluated, the next step in the recursion is not. This is what I get on the console.
*hello> windowl 2 [1,2,3,4,5]
[1, 2] :: Main.windowl, loop Integer 2 [2, 3, 4, 5] : List (List Integer)
Can someone enlighten me as to what is happening and how I can get the function evaluated completely?