diff options
Diffstat (limited to 'src/Data/Vect')
| -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 |