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 .

Going home
Pierre Castéran