The last element of a list
Define the inductive predicate (last A a l) meaning
l is a list of terms of type A and a is the
last item of l
Define a function last_fun of type
(list A -> option A) which returns the last element of a
list (if it exists).
Then show the consistency between both definitions.
Look at this file .