How do I evaluate this recursive function in Idris interactive?

Viewed 297

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?

1 Answers
Related