printing numerals

Stream: general

[Johan Commelin]

If I make a new type (copy of nat, for my son) and I ask it to #reduce plus honderd honderd it doesn't print 200 but ... .plus1.plus1.plus1.
I've created has_zero, has_one, and has_add instances.
What else do I need to do, to teach Lean to print numerals?

[Ruben Van de Velde]

bit0/bit1, maybe?

[Johan Commelin]

It already accepts numerals as input, because of those classes. But I guess I now need to teach it a has_repr or something. Is that right?

[Kevin Buzzard]

Maybe look at nat.has_repr? But numerals might be special. Just cast to nat with the repr maybe

[Sebastian Ullrich]

has_repr is for VM values, #reduce uses the pretty printer. It looks like there is special support for pretty printing nat.succ^k nat.zero, but for your own type you are out of luck in Lean 3.

[Johan Commelin]

Ooh oh, that's sad :sob:
We'll manage. He's pretty fascinated by unary notation at the moment. "Computers are soooo stupid. It's printing 99 by saying nul.plus1.plus1.plus1.... rotflol rotflol hihihi"

[Eric Wieser]

You can do something a bit silly with notation to make it slightly shorter:

inductive mynat
| zero
| plus1 (n : mynat)

def mynat_add : ∀ (a b : mynat), mynat
| mynat.zero b := b
| (mynat.plus1 a) b := mynat_add a b.plus1
instance : has_add mynat := ⟨mynat_add⟩

instance : has_zero mynat := ⟨mynat.zero⟩
instance : has_one mynat := ⟨mynat.zero.plus1⟩

local notation `ₘ0` := mynat.zero
local notation a ` +` ` ₘ1` := (mynat.plus1 a)
local notation a ` +` ` ₘ10` := mynat.plus1 $ mynat.plus1 $ mynat.plus1 $ mynat.plus1 $ mynat.plus1 $
                               mynat.plus1 $ mynat.plus1 $ mynat.plus1 $ mynat.plus1 $ mynat.plus1 a

#reduce (15 : mynat)  -- ₘ0 + ₘ1 + ₘ1 + ₘ1 + ₘ1 + ₘ1 + ₘ10

[Eric Wieser]

You could even write a metaprogram to spit out local notation for all the numbers between 0 and 1000

[Eric Wieser]

But it might not be the pedagogical exercise you were hoping for!

[Kevin Lacker]

maybe instead of defining the naturals based on the "successor" operation, you should define it based on the 2x and 2x+1 operations, and then it'll print more nicely

[Kevin Lacker]

inductive mypos
| one
| twice (n : mypos)
| twiceplusone (n : mypos)