[Agda] summing rationals

[Sergei Meshveliani]

On Mon, 2017-06-26 at 15:52 +0200, Nils Anders Danielsson wrote:
> 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".
> 

It is all the same. My comment had the following meaning. 
As (f n) is a fraction with a very large denominator, and the test
prints out  (f n) - (f n),  then this last subtraction costs much.
And its cost even occurs a bit more than the cost of all the rest
computation in the test.    

------
Sergei