[Agda] result code performance

[Ulf Norell]

On Tue, Sep 20, 2016 at 3:02 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

>
> And GHC is faster in a constant ratio of about 10.
> I think this is due to the difference between unary coding arithmetic in
> Agda's Standard library and n-ary one of GHC.
> For example,  12 * 12  costs 12 additions in DoCon-A and, probably, 3-4
> machine instructions in GHC
> (do I understand right of what is happening there ?).
>

No, natural number operations (_+_, _*_ etc) are compiled to the
corresponding
Haskell Integer operations.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160920/eefce067/attachment.html