diff options
Diffstat (limited to 'Ch10.idr')
-rw-r--r-- | Ch10.idr | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -21,5 +21,11 @@ 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 |