import Data.List
fsts : List (a,b) -> List a
fsts [] = []
fsts ((x, y) :: xs) = x :: fsts xs
prod : List Int -> Int
prod [] = 1
prod (x::xs) = x * prod xs
-- standardteegis map
my_map : (a -> b) -> List a -> List b
my_map f [] = []
my_map f (x::xs) = f x :: my_map f xs
inverses : List Double -> List Double
inverses xs = my_map inverse xs
where inverse : Double -> Double
inverse x = 1 / x
test1 : inverses [1,2,4,8] = [1.0, 0.5, 0.25, 0.125]
test1 = Refl
-- standardteegis foldr
my_foldr : (a -> b -> b) -> b -> List a -> b
my_foldr f b [] = b
my_foldr f b (x::xs) = f x (my_foldr f b xs)
prod' : List Int -> Int
prod' xs = my_foldr (*) 1 xs
my_map2 : (a -> b) -> List a -> List b
my_map2 f xs = my_foldr g [] xs
where g : a -> List b -> List b
g x y = (f x) :: y
test2 : my_map2 (+2) [1,2,3] = [3,4,5]
test2 = Refl
-- standardteegis foldl
my_foldl : (b -> a -> b) -> b -> List a -> b
my_foldl f b [] = b
my_foldl f b (x::xs) = my_foldl f (f b x) xs
-- standardteegis reverse
my_reverse : List a -> List a
my_reverse xs = my_foldl g [] xs
where g : List a -> a -> List a
g x y = y :: x
test3 : my_reverse [1,2,3] = [3,2,1]
test3 = Refl
f1 : List Int -> Int
f1 xs = sum (takeWhile (/= 0) xs)
f2 : List Int -> Int
f2 = sum . takeWhile (/= 0)
test4 : f1 [3,2,1,0,2,3,4] = 6
test4 = Refl
max3 : Int -> Int -> Int -> Int
max3 = (. max) . ((.) . max)
test5 : max3 2 3 1 = 3
test5 = Refl
test6 : map (\ x => x+1) [1,2,3,4] = [2,3,4,5]
test6 = Refl