-- Compute last element of a list (functional logic variant):
last :: Data a => [a] -> a
last xs | xs =:= _ ++ [x] = x
where x free
-- Compute last element of a list (functional variant):
lastF :: [a] -> a
lastF [x] = x
lastF (_ : xs@(_:_)) = lastF xs
-- verify correctness of functional variant: lastF (xs ++ [x]) -->* x
-- (for all xs and x)
-- use this as a constructive definition with functional pattern:
lastFP (xs ++ [x]) = x
-- This corresponds to:
{-
lastFP [x] = x -- if xs |-> []
lastFP [z1,x] = x -- if xs |-> [z1]
lastFP [z1,z2,x] = x -- if xs |-> [z1,z2]
...
-}