[Agda] no-built-in version

[Sergei Meshveliani]

Dear Agda team,

The current Standard library (lib-0.14) uses a built-in arithmetic for
Nat, and certain other built-in items.

But it has sense to _also_ have a no-built-in version.
Because there everything is proved down to bottom
(and let the unary arithmetic evaluate  51 + 103  in 52 pattern matching
steps). 
 
In my Bin3 library for Bin, I need to test the performance of certain
operations with Bin, in a situation when everything needed is proved. 
But Standard library is involved, with certain its  operations on ℕ. And
these latter are performed as built in. This breaks the performance
test.
Then I tried to copy a piece of Standard library and make it free from
built-ins, and to use in Bin3.
But this Standard library transformation occurs too difficult for me,
technically, too many obstacles.

So that now I am trying my home-made toNat that is equivalent to toℕ,
but has  cost(x) = O( 2^ (bitLength x) )  -- as it is in the naive unary
arithmetic.
I do not know, how will this work. Anyway this is not a regular
approach.

Generally:  
please, can a pure no-built-in version of Standard library be
provided?  

Regards,

------
Sergei