From c305e99c3f0866d2aa4fb0431b06fc398663bd94 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 25 Jul 2023 16:32:51 +0100
Subject: Remove SFin.

Delete unused modules.

Restructure some proofs to reduce the number of lemmas.
---
 src/Data/Vect/Properties/Insert.idr | 26 --------------------------
 1 file changed, 26 deletions(-)
 delete mode 100644 src/Data/Vect/Properties/Insert.idr

(limited to 'src/Data/Vect/Properties')

diff --git a/src/Data/Vect/Properties/Insert.idr b/src/Data/Vect/Properties/Insert.idr
deleted file mode 100644
index 28393b1..0000000
--- a/src/Data/Vect/Properties/Insert.idr
+++ /dev/null
@@ -1,26 +0,0 @@
-module Data.Vect.Properties.Insert
-
-import Data.Vect
-
-export
-mapInsertAt :
-  (0 f : a -> b) ->
-  (i : Fin (S n)) ->
-  (0 x : a) ->
-  (xs : Vect n a) ->
-  map f (insertAt i x xs) = insertAt i (f x) (map f xs)
-mapInsertAt f FZ x xs = Refl
-mapInsertAt f (FS i) x (y :: xs) = cong (f y ::) $ mapInsertAt f i x xs
-
-export
-indexInsertAt : (i : Fin (S n)) -> (0 x : a) -> (xs : Vect n a) -> index i (insertAt i x xs) = x
-indexInsertAt FZ x xs = Refl
-indexInsertAt (FS i) x (y :: xs) = indexInsertAt i x xs
-
-export
-insertAtIndex :
-  (i : Fin (S n)) ->
-  (xs : Vect (S n) a) ->
-  insertAt i (index i xs) (deleteAt i xs) = xs
-insertAtIndex FZ (x :: xs) = Refl
-insertAtIndex (FS i) (x :: xs@(_ :: _)) = cong (x ::) $ insertAtIndex i xs
-- 
cgit v1.2.3