Skip to content
Snippets Groups Projects

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

Merged Pretty-print 0 as "0" for N, Z, and nat
robbert/pretty_0 into master
All threads resolved!
Merged Robbert Krebbers requested to merge robbert/pretty_0 into master
All threads resolved!

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

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Robbert Krebbers added 4 commits

    added 4 commits

    • 1855e425 - Fix `pretty` for `N`.
    • 359bdf0f - Fix `pretty` for `Z` and prove `injectivity` of it.
    • 2b610e92 - Test cases for `pretty` of `N`, `nat`, and `Z`.
    • a73ac825 - CHANGELOG.

    Compare with previous version

    Toggle commit list
  • Robbert Krebbers resolved all threads

    resolved all threads

  • Robbert Krebbers merged

    merged

  • Robbert Krebbers mentioned in commit 92b285f8

    mentioned in commit 92b285f8

  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers ·
    Author Owner

    Merged. Many thanks for the initial MR @tchajed!

  • Tej Chajed mentioned in merge request iris!564 (merged)

    mentioned in merge request iris!564 (merged)

    • Please register or sign in to reply