On 2017-06-25 16:26, Sergei Meshveliani wrote: > 1. It appears that final fn - fn in my test costs as much as all the > rest. As far as I know Agda transforms "let fn = f n in fn - fn" into "f n - f n". -- /NAD