blob: 1ef5a45feab3dd5c16af204d31e6de5ecd6022b6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
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
|
