diff options
-rw-r--r-- | Ch10.idr | 30 |
1 files changed, 25 insertions, 5 deletions
@@ -1,9 +1,5 @@ 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) @@ -27,5 +23,29 @@ takeDropIsIdentity Z input = Refl takeDropIsIdentity (S k) [] = Refl takeDropIsIdentity (S k) (x :: xs) = rewrite takeDropIsIdentity k xs in Refl + +mySplitPreservesElements : (n : Nat) -> (input : List a) -> ((ps, qs) = mySplit n input) -> ps ++ qs = input +mySplitPreservesElements n input prf = + let prf2 = mySplitIsTakeDrop n input in + case trans prf prf2 of Refl => takeDropIsIdentity n input + +data Partition : List a -> Type where + Split : (xs, ys : List a) -> Partition (xs ++ ys) -takeN : (n : Nat) -> (input : List a) -> TakeN input +test : (input : List a) -> Partition input +test zs = + let (xs, ys) = mySplit 5 zs in ?test + + +data TakeN : List a -> Type where + Fewer : TakeN xs + Exact : (n_xs : List a) -> TakeN (n_xs ++ rest) + +-- takeN : (n : Nat) -> (input : List a) -> TakeN input +-- takeN n input = +-- let (n_xs, rest) = mySplit n input in +-- let prf0 = mySplitPreservesLength n input ?foo in +-- let prf = the (n_xs ++ rest = input) ?my in +-- if length n_xs < n +-- then Fewer +-- else ?hole |