[Agda] summing rationals

Nils Anders Danielsson nad at cse.gu.se
Mon Jun 26 15:52:15 CEST 2017


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


More information about the Agda mailing list