Appending Two Lists

We want to be able to append (concatenate) one list on to the end of another. To do this we define the append function.

append: list alpha # list alpha -> list alpha

The append function takes two lists as parameters and returns the list consisting of the second list `stuck on' the end of the first list. As you might now expect, append is defined recursively. There are two rules for the append function. The first rule is when the left hand list is empty in which case we simply return the second list. i.e.

append ([],k) <= k;

The second rule is for when the left hand list is not empty. In which case, we recursively append the tail of the left list to the right list and then cons the head of the left list onto the result:

append (x::m,k) <= x::append(m,k);