From 6aa16c40df3cd44b8a6d47f6153e28c892f4dee9 Mon Sep 17 00:00:00 2001
From: Kjetil Orbekk <kjetil.orbekk@gmail.com>
Date: Tue, 14 Feb 2017 08:35:27 -0500
Subject: Add Ch10 exercise.

---
 Ch10.idr | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 Ch10.idr

diff --git a/Ch10.idr b/Ch10.idr
new file mode 100644
index 0000000..1ef5a45
--- /dev/null
+++ b/Ch10.idr
@@ -0,0 +1,20 @@
+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
-- 
cgit v1.2.3