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: Aug 03 2023 at 10:10 UTC