Skip to content

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

Robbert Krebbers requested to merge robbert/pretty_0 into master

Alternative to #198 (closed) 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 by Robbert Krebbers

Merge request reports