Skip to content
GitLab

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

Merged Robbert Krebbers requested to merge robbert/pretty_0 into master

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 by Robbert Krebbers