diff options
Diffstat (limited to 'Ch10.idr')
-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 |