1. Dla wektorów napisz:
 
a) my_vect_map : (a -> b) -> Vect n a -> Vect n b
b)insert : Ord elem => (x : elem) -> (xsSorted : Vect k elem) -> Vect (S k) elem
c) insertion sort

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

pamiętaj o import Data.Vect

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

Używając:

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

oraz

Napisz funkcje: 

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

1 2 3
4 5 6

na

1 4
2 5
3 6

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

c) multMatrix : Num a => {p: _} -> Vect m (Vect n a) -> Vect n (Vect p a) -> Vect m (Vect p a)

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) odpowiednik take dla list
c) sumEntriesAt : Num a => {n: _} -> (pos : Integer) -> Vect n a -> Vect n a -> Maybe a


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

5. Zdefiniuj wectory używając zagnieżdżonych krotek, tak żeby

TupleVect 0 ty = ()
TupleVect 1 ty = (ty, ())
TupleVect 2 ty = (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.