myReverse :: [a] -> [a]
myReverse []     = []
myReverse (x:xs) = myReverse xs ++ [x]

(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x:xs ++ ys

myReverse [1,2,3]
= {notation}
myReverse (1:2:3:[])
= {application de myReverse}
myReverse (2:3:[]) ++ [1]
= {application de myReverse}
(myReverse (3:[]) ++ [2]) ++ [1]
= {application de myReverse}
((myReverse [] ++ [3]) ++ [2]) ++ [1]
= {application de myReverse}
(([] ++ [3]) ++ [2]) ++ [1]
= {application de (++)}
([3] ++ [2]) ++ [1]
= {notation}
((3:[]) ++ [2]) ++ [1]
= {application de (++)}
3:([] ++ [2]) ++ [1]
= {application de (++)}
3:[2] ++ [1]
= {notation}
3:2:[] ++ [1]
= {application de (++)}
3:(2:[] ++ [1])
= {application de (++)}
3:(2:([] ++ [1]))
= {application de (++)}
3:(2:[1])
= {notation}
[3,2,1]


myReverse' :: [a] -> [a]
myReverse' xs = aux xs []
  where aux []     ys = ys
        aux (x:xs) ys = aux xs (x:ys)

myReverse' [1,2,3]
= {application de myReverse'}
aux [1,2,3] []
= {notation}
aux (1:2:3:[]) []
= {application de aux}
aux (2:3:[]) (1:[])
= {application de aux}
aux (3:[]) (2:1:[])
= {application de aux}
aux [] (3:2:1:[])
= {application de aux}
3:2:1:[]
= {notation}
[3,2,1]


myFoldr :: (a -> b -> b) -> b -> [a] -> b
myFoldr op base []     = base
myFoldr op base (x:xs) = x `op` myFoldr op base xs

x:y:z:[] = x:(y:(z:[]))

myFoldr op base [x,y,z]
= {notation}
myFoldr op base (x:y:z:[])
= {application de myFoldr}
x `op` myFoldr op base (y:z:[])
= {application de myFoldr}
x `op` (y `op` myFoldr op base (z:[]))
= {application de myFoldr}
x `op` (y `op` (z `op` myFoldr op base []))
= {application de myFoldr}
x `op` (y `op` (z `op` base))

x:(y:(z:[])) ---> x `op` (y `op` (z `op` base))
x:(y:(z:[])) ---> x `cons` (y `cons` (z `cons` nil))