ex_3_2_4.idr

import Data.Vect

total my_length : List a -> Nat
my_length [] = 0
my_length (x :: xs) = S (my_length xs)

append : List a -> a -> List a
append [] y = [y]
append (x :: xs) y = x :: (append xs y)

total my_reverse : List a -> List a
my_reverse [] = []
my_reverse (x :: xs) = let reversed = my_reverse xs in 
                           append reversed x
                           
total my_reverse_efficient : List a -> List a
my_reverse_efficient xs = inner xs []
  where
    inner: List a -> List a -> List a
    inner [] ys = ys
    inner (x :: xs) ys = inner xs (x :: ys)
    
total my_map : (a -> b) -> List a -> List b
my_map f [] = []
my_map f (x :: xs) = let mapped = my_map f xs in
                         f x :: mapped

total my_vect_map : (a -> b) -> Vect n a -> Vect n b
my_vect_map f [] = []
my_vect_map f (x :: xs) = let mapped = my_vect_map f xs in
                              f x :: mapped