memory model of natural numbers

Stream: lean4

[Schrodinger ZHU Yifan]

Is it true that all lean_nat related API does not "consume" the object except for those declared with dec?

[James Gallicchio]

I don't entirely understand the question, but I'll try to explain a bit -- for x : Nat there's two possible memory representations.

• If x < 2^63, it is represented as the uint64 value (n << 1) + 1
• If x >= 2^63 it is represented as a lean_object* which contains a libgmp int.

So, since the objects might not be scalars, lean_inc and lean_dec are still called to maintain reference counts in the case where it's not scalar.

[Mario Carneiro]

As far as I can tell, the answer is yes (I don't see any lean_nat functions containing dec except lean_nat_dec_eq which is an unrelated use of dec). I'll make a PR to update lean.h with more accurate borrowing annotations

[James Gallicchio]

all the lean_nat functions I see take b_lean_obj_arg..? is there one that isn't accurate?

[Mario Carneiro]

lean_nat_big_succ takes object* for example

[James Gallicchio]

oh, all the lean_nat_big functions, i see