# Computing *f(0)+f(1)+...f(n)*

Define the functional which maps a function *f* from
`nat` to `Z` to the sum
*f(0)+f(1)+...f(n)*
## Solution

Look at this file
### Note

The solution comes with a little example, which uses some tactics
to control the relationship between `nat` and `Z`.

Going home

Pierre Castéran