Bypass lean functions with lean functions at runtime?

Stream: lean4

[Michael Jam]

Hello. When I see that:

@[extern "lean_nat_add"]
protected def Nat.add : (@& Nat) → (@& Nat) → Nat

My understanding is that the code lean uses at execution time is not the code in Nat.add's body, but it is an external piece of C++ code that will run very fast. This way lean can perform fast computations on structures which appear inefficient as they are represented in lean. Nat.add's code is not efficient, but it uses the inductive structure, because it is much easier to prove things this way.

Is there something similar for lean functions?
Can I bypass at runtime a lean function, with another optimized lean function with same signature? (possibly providing a proof that the two versions are equivalent)
Or is it wrong to want something like that ?

Some benefits I thought of are that for some primitive functions, I can have one version with good def behavior, and another version with good runtime performance.
Next I could write more complex functions in terms of the well defined primitive functions only. I might not need to write an optimized complex function in terms of optimized primitive functions, because it might run fast enough already.
I'm saying all that as I saw some tail recursive functions in the standard library, I think tail recursivity make things faster to run, but I'm afraid it might be a distraction for proof writing...

[Gabriel Ebner]

def three := 3

@[implementedBy three]
def fourtyTwo := 42

#eval fourtyTwo -- 3

[Michael Jam]

Ok there is something already. Thanks!