@@ -113,6 +113,21 @@ index' Z (x::xs) = Just x
113index' (S n) (x::xs) = index' n xs
113index' (S n) (x::xs) = index' n xs
114index' _ [] = Nothing
114index' _ [] = Nothing
116+||| Delete a particular element of a list.
117+deleteAt : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> List a
118+deleteAt Z (_ :: xs) = xs
119+deleteAt (S n) (x :: xs) {ok = InLater ok} = x :: deleteAt {ok} n xs
121+||| Insert an element into a list at a particular point.
122+insertAt : (n : Nat) -> a -> (xs : List a) -> {auto ok : InBounds n xs} -> List a
123+insertAt Z elem xs = elem :: xs
124+insertAt (S n) elem (x :: xs) {ok = InLater ok} = x :: insertAt {ok} n elem xs
126+||| Replace a particular element of a list.
127+replaceAt : (n : Nat) -> a -> (xs : List a) -> {auto ok : InBounds n xs} -> List a
128+replaceAt Z elem (_ :: xs) = (elem :: xs)
129+replaceAt (S n) elem (x :: xs) {ok = InLater ok} = x :: replaceAt {ok} n elem xs
116||| Get the first element of a non-empty list
131||| Get the first element of a non-empty list
117||| @ ok proof that the list is non-empty
132||| @ ok proof that the list is non-empty
118head : (l : List a) -> {auto ok : NonEmpty l} -> a
133head : (l : List a) -> {auto ok : NonEmpty l} -> a
@@ -885,3 +900,20 @@ foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q x
885foldlMatchesFoldr f q [] = Refl
900foldlMatchesFoldr f q [] = Refl
886foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
901foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
903+replaceIsDeleteAndInsert : insertAt {ok=ok1} n x (deleteAt {ok=ok2} n xs) = replaceAt {ok=ok3} n x xs
904+replaceIsDeleteAndInsert {xs = []} {ok3 = InFirst} impossible
905+replaceIsDeleteAndInsert {xs = []} {ok3 = InLater _} impossible
906+replaceIsDeleteAndInsert {xs = _ :: _} {ok3 = InFirst} = Refl
907+replaceIsDeleteAndInsert {xs = _ :: _} {ok3 = InLater _} {ok2 = InFirst} impossible
908+replaceIsDeleteAndInsert {xs = _ :: _} {ok3 = InLater _} {ok1 = InFirst} impossible
909+replaceIsDeleteAndInsert {xs = x :: xs} {ok3 = InLater ok3} {ok1 = InLater ok1} {ok2 = InLater ok2} =
910+ cong (replaceIsDeleteAndInsert {ok1} {ok2} {ok3})
912+deleteOppositeInsert : deleteAt {ok=ok1} n (insertAt {ok=ok2} n x xs) = xs
913+deleteOppositeInsert {xs = []} {ok2 = InFirst} impossible
914+deleteOppositeInsert {xs = []} {ok2 = InLater _} impossible
915+deleteOppositeInsert {xs = _ :: _} {ok2 = InFirst} = Refl
916+deleteOppositeInsert {xs = _ :: _} {ok1 = InLater _} {ok2 = InFirst} impossible
917+deleteOppositeInsert {xs = x :: xs} {ok1 = InLater ok1} {ok2 = InLater ok2} =
918+ cong (deleteOppositeInsert {ok1} {ok2})