Definition: The function \(prepend : L \times \mathbb{N} \to L\) that adds an element at the front of a linked list is defined by \[\phantom{prepend(~(l, n)~) = (n, l)}\]