On the list 1::2:: ... n::nil

Build a function computing the list 1::2:: ... n::nil for every n of type nat.


Look at this file


This solution uses an anonymous recursive function (with fix). If you want to prove some properties of the main function, it could be useful to give a name to this auxiliary function (i.e to define it with Fixpoint).

Going home
Pierre Castéran