Zulip Chat Archive

Stream: general

Topic: internal representation of natural numbers

Huỳnh Trần Khanh (Jul 15 2021 at 05:22):

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 (Jul 15 2021 at 05:23):

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

Johan Commelin (Jul 15 2021 at 05:30):

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

Eric Wieser (Jul 15 2021 at 08:22):

#reduce also works I think

Last updated: Dec 20 2023 at 11:08 UTC