WIP: Pretty-print 0 as "0" for N, Z, and nat

Formerly printed as an empty string.

mentioned in merge request iris!564 (merged)

Since we don't prove any properties that establish the correctness of this function (apart from it being injective), it would be great to add a couple of tests. Maybe in tests/pretty.v or so? Would you want to do that?

Good point, especially because this fix is incorrect (it makes pretty 1 = "10").

How many computer scientists does it take to write a correct pretty printer for natural numbers?

At least 2, it seems...

Wow this is actually really difficult. We can't easily write a recursive pretty-printer for positive because division and modulo won't work, so we basically need to wrap the current definition in a layer that checks for 0.

marked as a Work In Progress

Welp, I tried to prove that pretty_N_go x "" doesn't equal 0 as a stepping stone to proving that the new pretty_N x is injective and this turns out be too hard for me to do right now.

As discussed with @tchajed, I created an alternative MR. See !200 (merged). Closing this one.

closed

mentioned in commit a73ac825

mentioned in commit 1855e425