Est-ce que j'utilise un bon raisonnement équationnel sur une définition de filtre en termes de foldr ?

Question

Voici la définition de la fonction de filtrage en utilisant foldr :

myFilter p xs = foldr step [] xs
    where step x ys | p x       = x : ys
                    | otherwise = ys

Donc, par exemple, disons que j'ai cette fonction :

myFilter odd [1,2,3,4]

il en sera ainsi :

foldr step [] [1,2,3,4]

et ce sera

step 1 (foldr step [] [2,3,4])

et ce sera

step 1 (step 2 (foldr step [] [3,4]))

et ce sera

step 1 (step 2 (step 3 (foldr step [] [4])))

et ce sera

step 1 (step 2 (step 3 (step 4 (foldr step [] []))))

et foldr step [] [] es [] donc :

step 1 (step 2 (step 3 (step 4 [])))

Nous allons maintenant entrer dans le step fonction.
voici la définition de step à l'intérieur de la myFilter fonction, depuis le haut :

step x ys | p x       = x : ys
          | otherwise = ys

Aussi, je vous rappelle que p est en fait le odd dans notre exemple.

Eh bien, encore une fois, nous sommes ici :

step 1 (step 2 (step 3 (step 4 [])))

et

x = 4 au plus profond step et 4 n'est pas impair, donc nous retournons ys qui est []

donc maintenant on a ça :

step 1 (step 2 (step 3 []))

maintenant, au plus profond step , x = 3 et 3 est impair, donc nous retournons x:ys qui est 3 : [] qui est [3] et maintenant nous avons :

step 1 (step 2 [3])

et maintenant, dans l'intérieur step , x = 2 et 2 n'est pas impair, donc nous retournons ys qui est [3] donc maintenant nous aurons :

step 1 [3]

et maintenant, x = 1 et 1 est impair, donc nous retournons x : ys qui est 1 : [3] qui est [1,3] .

La fin :-).

Est-ce que j'ai raison dans tous mes mouvements ?
Merci beaucoup :-).

p.s. la définition de myFilter est tiré du livre Haskell dans le monde réel dans le chapitre 4.