module Ch10

data TakeN : List a -> Type where
  Fewer : TakeN xs
  Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)
 
mySplit : (n : Nat) -> (input : List a) -> (List a, List a)
mySplit n [] = ([], [])
mySplit Z xs = ([], xs)
mySplit (S k) (x :: xs) = let (this, rest) = (mySplit k xs) in
                          (x :: this, rest)
                          
mySplit_keeps_list : (n : Nat) -> (input : List a) ->
                     mySplit n input = (as, bs) -> as ++ bs = input
mySplit_keeps_list Z [] Refl = Refl
mySplit_keeps_list (S k) [] Refl = Refl
mySplit_keeps_list Z (x :: xs) Refl = Refl
mySplit_keeps_list (S k) (x :: xs) prf = ?hole  -- ????

takeN : (n : Nat) -> (input : List a) -> TakeN input