@@ -113,21 +113,6 @@ index' Z (x::xs) = Just x
113113index' (S n) (x::xs) = index' n xs
114114index' _ [] = Nothing
115115
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
120−
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
125−
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
130−
131116||| Get the first element of a non-empty list
132117||| @ ok proof that the list is non-empty
133118head : (l : List a) -> {auto ok : NonEmpty l} -> a
@@ -900,20 +885,3 @@ foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q x
900885foldlMatchesFoldr f q [] = Refl
901886foldlMatchesFoldr f q (x :: xs) = foldlMatchesFoldr f (f q x) xs
902887
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})
911−
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})
919−