diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-07-25 16:32:51 +0100 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-07-25 16:32:51 +0100 |
| commit | c305e99c3f0866d2aa4fb0431b06fc398663bd94 (patch) | |
| tree | c1dcc5321816c953b11f04b27b438c3de788970c /src/Data/Vect/Properties/Insert.idr | |
| parent | bb4e7c82b7ecd93b7241be5fcc547cfd282a8908 (diff) | |
Remove SFin.
Delete unused modules.
Restructure some proofs to reduce the number of lemmas.
Diffstat (limited to 'src/Data/Vect/Properties/Insert.idr')
| -rw-r--r-- | src/Data/Vect/Properties/Insert.idr | 26 |
1 files changed, 0 insertions, 26 deletions
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 |