1. Dla wektorów napisz:
 
a) my_vect_map : (a -> b) -> Vect n a -> Vect n b
b) insert, który wsortowuje element x do posortowanej listy

insert : Ord el => (x : el) -> (xsSorted : Vect k el) -> Vect (S k) el

c) insertion sort, używając insert z poprzedniego podpunktu

insSort : Ord el => Vect n el -> Vect n el 

pamiętaj o import Data.Vect

2. Załóżmy, że typ macierzy nxm (n wierszy m kolumn) o wartościach w typie el reprezentowany jest przez Vect n (Vect m el). 

Używając:

create_empties : {n : Nat} -> Vect n (Vect 0 el)
create_empties {n = Z} = []
create_empties {n = (S k)} = [] :: create_empties


Napisz funkcje: 

a) transpose_mat : {n : Nat} -> Vect m (Vect n el) -> Vect n (Vect m el)
zamieniającą macierz 

1 2 3
4 5 6

na

1 4
2 5
3 6

b) addMatrix : Num el => Vect n (Vect m el) -> Vect n (Vect m el) -> Vect n (Vect m el)

c) multMatrix : Num el => {p: Nat} -> Vect m (Vect n el) -> Vect n (Vect p el) -> Vect m (Vect p el)

Wskazówka do c) zacznij od transpose_mat prawej macierzy 

3. Obejrzyj typ Fin i funkcje integerToFin i index
 
(:module Data.Vect, :doc Fin, :t integerToFin, :t index)

sprawdź wartości:

integerToFin 0 4
integerToFin 1 4
integerToFin 2 4
integerToFin 3 4
integerToFin 4 4

Napisz funkcje:

a) tryIndex : {n: _} -> Integer -> Vect n a -> Maybe a
b) vectTake - odpowiednik take dla list, biorący pod uwagę długości wektorów
c) sumEntriesAt : Num a => {n: _} -> (pos : Integer) -> Vect n a -> Vect n a -> Maybe a

sumująca wartości z dwóch wektorów pod indeksami pos

4. Obejrzyj plik Printf.idr i rozszerz o formaty dla Char i Double

5. Zdefiniuj funkcję TupleVect : Nat -> Type -> Type,
budującą typ wektorów o danej długości, używając zagnieżdżonych krotek: 

(TupleVect 0 ty) to ma być typ  ()
(TupleVect 1 ty) to ma być typ  (ty, ())
(TupleVect 2 ty) to ma byc typ  (ty, (ty, ()))
....

Czyli zdefiniuj funkcję obliczającą typy
      TupleVect: Nat -> Type -> Type
, tak żeby:

test : TupleVect 4 Nat
test = (1,2,3,4,())

Napisz appendTV dla takich wektorów.