internal representation of natural numbers

Stream: general

[Huỳnh Trần Khanh]

of course natural numbers are not represented internally in the Peano form right? because otherwise Lean couldn't handle numbers such as 2147483647 in reasonable time :cry: so... how can I see that internal representation then? #print doesn't help...

[Huỳnh Trần Khanh]

it looks like bit0 (bit1 (bit0 (bit1 0))) right?

[Johan Commelin]

Is there some set_option pp.numerals false that you can invoke? I think it was something like that.

[Eric Wieser]

#reduce also works I think