Does Lean contain numerical bases?

Stream: new members

[Abhimanyu Pallavi Sudhir]

Specifically, I want a way to extract the base-n digits of a number as a list. Does this already exist?

[Andrew Ashworth]

that seems pretty specialized, so i doubt it

[Kenny Lau]

#eval nat.to_digits 2 100 --[0, 0, 1, 0, 0, 1, 1]

[Andrew Ashworth]

woah, i'm wrong

[Chris Hughes]

That's just there so numerals can be printed and parsed.

[Bryan Gin-ge Chen]

Here it is in core lean. As a newbie to functional programming, I thought this was super cool.

[Kevin Buzzard]

oh so that's how repr works :-)

[Kevin Buzzard]

def nat.repr2 (n : ℕ) : string :=
((nat.to_digits 2 n).map nat.digit_char).reverse.as_string

@[priority 10000]
instance nat.has_repr2 : has_repr nat :=
⟨nat.repr2⟩

#eval 7 -- 111

woo I have binary Lean!

[Chris Hughes]

Hide that in xenalib somwhere and confuse everyone.

[Abhimanyu Pallavi Sudhir]

#eval nat.to_digits 2 100 --[0, 0, 1, 0, 0, 1, 1]

Nice!

[Kevin Buzzard]

The way to find it is to think "hmm, how are naturals being printed?" then "hmm, what is the definition of nat.repr?"