diff options
Diffstat (limited to 'Ch10.idr')
-rw-r--r-- | Ch10.idr | 25 |
1 files changed, 15 insertions, 10 deletions
@@ -3,18 +3,23 @@ module Ch10 data TakeN : List a -> Type where Fewer : TakeN xs Exact : (n_xs : List a) -> TakeN (n_xs ++ rest) - + +splitStep : a -> (List a, List a) -> (List a, List a) +splitStep x (xs, ys) = (x :: xs, ys) + 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 -- ???? +mySplit (S k) (x :: xs) = splitStep x (mySplit k xs) + +mySplitIsTakeDrop : (n : Nat) -> (input : List a) -> + mySplit n input = (take n input, drop n input) +mySplitIsTakeDrop Z [] = Refl +mySplitIsTakeDrop Z (x::xs) = Refl +mySplitIsTakeDrop Z [] = Refl +mySplitIsTakeDrop (S k) [] = Refl +mySplitIsTakeDrop (S k) (x::xs) = + let rec = mySplitIsTakeDrop k xs in + rewrite rec in Refl takeN : (n : Nat) -> (input : List a) -> TakeN input |