sum: list(num) -> num; sum [ ] <= 0; sum(x::m) <= x + sum(m);We read this as follows: The sum of the empty list of integers is zero. To sum the list of integers whose head is
xand whose tail is
m, we sum the tail,
mand add the head
xto the result.
How is this evaluated? Suppose we ask Hope to evaluate
 is the list whose head is 2 and whose tail is
sum=sum(2::). This matches the second rule for sum with
So we rewrite the right hand side of the second rule with
m= to give
By the first rule for
so the result of
2+0 which is 2.