blob: 9ab70ce2e9cbcbc694e10a4da615300383b6b018 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
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) = 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
|
