Provide a pretty-printer for [nat].

Pretty-print nat; this simply reduced to the N pretty printer.

I think it would be better to define an injective instance for Nat2N.inj (which is useful on its own). Then this lemma can just be proven by unfold pretty, pretty_nat; apply _.

Oh, and thanks for the MR :)

Where would be the best place to add the Inj instances? Putting them in pretty doesn't feel right, but putting them in numbers means we'd have to import it just for this one instance.

I think importing numbers is fine.

added 1 commit

• e8560422 - Provide more Inj instances in numbers

Compare with previous version

I see you have updated the MR; it looks good to me.

It would be good to have a more principled look at whether we have injective instances for all conversion functions between number types now. Also note that the one for Z.of_nat is somewhere else in the file: It would be better to put them together. We can also do this later, and, as far as I am concerned, we can merge it.

Let's postpone the conversion function cleanup to later; I think there might be some more work to be done for that, e.g., making sure that we have injectivity proofs for each conversion function and so on.

mentioned in commit 88c82d21

merged

Merged, thanks!

FTR, the changes in pretty.v in this MR broke coqchk. That's not a complaint against this MR, but still interesting -- considering that the proofs it adds are tiny...