diff options
author | Kjetil Orbekk <kjetil.orbekk@gmail.com> | 2017-02-14 08:35:27 -0500 |
---|---|---|
committer | Kjetil Orbekk <kjetil.orbekk@gmail.com> | 2017-02-14 08:35:27 -0500 |
commit | 6aa16c40df3cd44b8a6d47f6153e28c892f4dee9 (patch) | |
tree | 50a551b01c52d345a404dbfc99e5f51704567318 | |
parent | 202ef8c368d08a3af27655e71772febdd7554351 (diff) |
Add Ch10 exercise.
-rw-r--r-- | Ch10.idr | 20 |
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 |