From 173b3078a963c18ddb005ea21237cce0cd718f79 Mon Sep 17 00:00:00 2001
From: Johannes Kloos <jkloos@mpi-sws.org>
Date: Tue, 31 Oct 2017 11:39:35 +0100
Subject: [PATCH] Provide a pretty-printer for [nat].

---
 theories/pretty.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/pretty.v b/theories/pretty.v
index 541e72a2..67dd8fd4 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -70,3 +70,10 @@ Instance pretty_Z : Pretty Z := λ x,
   match x with
   | Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x)
   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.
-- 
GitLab