-- Compute the last element of a list

-- Functional:
lastF [x]      = x
lastF (x:y:zs) = lastF (y:zs)
-- > To prove: last (xs ++ [x]) = x

-- Logic functional:
lastL xs | xs =:= _ ++ [x] = x
 where x free

-- With functional pattern:
lastFP (_ ++ [x]) = x

-------------------------------------------------------------
-- Non-linear functional pattern:

idpair x = (x,x)

f (idpair x) = 0

-- > f (x,x) = 0
-- > f (x,y) | x =:= y = 0

zero x = 0

pair x y = (x, y)

g (pair (zero x) x) = 0

-- > g (0,x) = 0