[Agda] result code performance

[Ulf Norell]

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

> On Tue, 2016-09-20 at 15:07 +0200, Ulf Norell wrote:
>
> > No, natural number operations (_+_, _*_ etc) are compiled to the
> > corresponding
> > Haskell Integer operations.
> >
>
> !?
> How new is this feature?
>

About a year old.

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