## Stream: new members

### Topic: Does Lean contain numerical bases?

#### Abhimanyu Pallavi Sudhir (Nov 09 2018 at 23:23):

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

#### Andrew Ashworth (Nov 09 2018 at 23:25):

that seems pretty specialized, so i doubt it

#### Kenny Lau (Nov 09 2018 at 23:25):

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


woah, i'm wrong

#### Chris Hughes (Nov 09 2018 at 23:27):

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

#### Bryan Gin-ge Chen (Nov 10 2018 at 00:19):

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

#### Kevin Buzzard (Nov 10 2018 at 00:45):

oh so that's how repr works :-)

#### Kevin Buzzard (Nov 10 2018 at 00:51):

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 (Nov 10 2018 at 01:12):

Hide that in xenalib somwhere and confuse everyone.

#### Abhimanyu Pallavi Sudhir (Nov 10 2018 at 12:41):

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


Nice!

#### Kevin Buzzard (Nov 10 2018 at 12:48):

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

Last updated: May 07 2021 at 00:30 UTC