summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKjetil Orbekk <kjetil.orbekk@gmail.com>2017-02-14 08:35:27 -0500
committerKjetil Orbekk <kjetil.orbekk@gmail.com>2017-02-14 08:35:27 -0500
commit6aa16c40df3cd44b8a6d47f6153e28c892f4dee9 (patch)
tree50a551b01c52d345a404dbfc99e5f51704567318
parent202ef8c368d08a3af27655e71772febdd7554351 (diff)
Add Ch10 exercise.
-rw-r--r--Ch10.idr20
1 files changed, 20 insertions, 0 deletions
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