blob: 075aba48f7184b4e08881e40e64aecab4c61126e (
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
26
27
28
29
30
31
|
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
takeDropIsIdentity : (n : Nat) -> (input : List a) -> take n input ++ drop n input = input
takeDropIsIdentity Z input = Refl
takeDropIsIdentity (S k) [] = Refl
takeDropIsIdentity (S k) (x :: xs) =
rewrite takeDropIsIdentity k xs in Refl
takeN : (n : Nat) -> (input : List a) -> TakeN input
|
