Zulip Chat Archive

Stream: new members

Topic: Does Lean contain numerical bases?


view this post on Zulip 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?

view this post on Zulip Andrew Ashworth (Nov 09 2018 at 23:25):

that seems pretty specialized, so i doubt it

view this post on Zulip Kenny Lau (Nov 09 2018 at 23:25):

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

view this post on Zulip Andrew Ashworth (Nov 09 2018 at 23:25):

woah, i'm wrong

view this post on Zulip Chris Hughes (Nov 09 2018 at 23:27):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 00:45):

oh so that's how repr works :-)

view this post on Zulip 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!

view this post on Zulip Chris Hughes (Nov 10 2018 at 01:12):

Hide that in xenalib somwhere and confuse everyone.

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 10 2018 at 12:41):

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

Nice!

view this post on Zulip 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