[Agda] Efficient numeric computations in Agda

[Arseniy Alekseyev]

Hello!

I am starting to learn Agda and trying to solve some Project Euler
problems with it.
To solve some of them one needs efficient number representation
(binary rather than unary).

The agda standard library seems not to provide such data types.
However, I'm sure someone uses them!
So, where should I dig to get such a library?
I could try and create bindings to the Haskell's Integer Num instance,
or design my own binary data type, but is one of those the way to go?

Another problem I had is the performance of Data.Nat.DivMod.divMod.
The source code says that its run time should be linear in the size of
dividend, but for me it's definitely quadratic.
I'm running the code from emacs' "Evaluate term to normal form" command.
Is that an appropriate way of running, or should I compile an
executable to see linear time?

Thank you,
Arseniy.