Skip to content
Snippets Groups Projects
Commit 173b3078 authored by Johannes Kloos's avatar Johannes Kloos
Browse files

Provide a pretty-printer for [nat].

parent 2e5cc41f
No related branches found
No related tags found
1 merge request!15Provide a pretty-printer for [nat].
Hide whitespace changes
Inline Side-by-side
Showing
with 7 additions and 0 deletions
theories/pretty.v
+ 7
− 0
View file @ 173b3078
...@@ -70,3 +70,10 @@ Instance pretty_Z : Pretty Z := λ x, ...@@ -70,3 +70,10 @@ Instance pretty_Z : Pretty Z := λ x,
match x with match x with
| Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x) | Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x)
end%string. end%string.
Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
Instance pretty_nat_inj : Inj (@eq nat) (=) pretty.
Proof.
unfold pretty, pretty_nat.
apply compose_inj with (R2 := eq) (f := N.of_nat), _.
exact Nat2N.inj.
Qed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment