Pretty-print 0 as "0" for N, Z, and nat (!200) · Merge requests · Iris / stdpp · GitLab

Merged Robbert Krebbers requested to merge robbert/pretty_0 into master Nov 09, 2020

Alternative to #198 that is correct. This MR also:

Adds test cases.
Proves injectivity of pretty for Z.
Refactored the code a bit by turning some results into lemmas.

Edited Nov 09, 2020 by Robbert Krebbers