[Agda] result code performance

[Sergei Meshveliani]

On Tue, 2016-09-20 at 15:07 +0200, Ulf Norell wrote:
> 
> 
> 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.
> 

!?
How new is this feature?

(I have seen some text about built-ins, but I could not understand that
this concerns the real run-time behavior).