On 2017-02-27 21:38, Sergei Meshveliani wrote: > when I expect that there the result for (add a (x ∷ xs)) must be > a ∷ x ∷ xs. The term "add a (x ∷ xs)" reduces to "aux (a ≟ 0) (x ∷ xs)", which is stuck, because "a ≟ 0" does not reduce to WHNF. (I think you forgot to send the message to which I am responding to the mailing list.) -- /NAD