From 72a5e4b58c29bb90495b6f9512c529a137ba29ee Mon Sep 17 00:00:00 2001
From: Kjetil Orbekk <kjetil.orbekk@gmail.com>
Date: Wed, 15 Feb 2017 08:02:06 -0500
Subject: Update split stuff.

---
 Ch10.idr | 30 +++++++++++++++++++++++++-----
 1 file changed, 25 insertions(+), 5 deletions(-)

diff --git a/Ch10.idr b/Ch10.idr
index 075aba4..b9e4714 100644
--- a/Ch10.idr
+++ b/Ch10.idr
@@ -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
-- 
cgit v1.2.3