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

Build a function computing the list 1::2:: ... n::nil for every n of type nat. Solution Look at this file Note 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

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

Solution

Note

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