Window.idr

-- http://stackoverflow.com/questions/44079181/idris-vect-fromlist-usage-with-generated-list

total
takeExact : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
takeExact Z xs = Just []
takeExact (S n) [] = Nothing
takeExact (S n) (x :: xs) with (takeExact n xs)
  takeExact (S n) (x :: xs) | Nothing = Nothing
  takeExact (S n) (x :: xs) | (Just v) = Just (x :: v)


total
window : (n : Nat) -> List a -> List (Vect n a)
window n xs with (takeExact n xs)
  window n xs | Nothing = []
  window n [] | (Just ys) = []
  window n (x :: xs) | (Just ys) = ys :: window n xs