From 0e0070eb2f660b1a54a99cce093fd00a0c066489 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rlewis1@andrew.cmu.edu>
Date: Wed, 7 Jun 2017 17:08:02 -0400
Subject: [PATCH] feat(reflect): add formatting instances and make nat.reflect
 0 a numeral

---
 library/init/meta/has_reflect.lean | 11 +++++++++--
 library/init/meta/tactic.lean      |  6 ++++++
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/library/init/meta/has_reflect.lean b/library/init/meta/has_reflect.lean
index 15b9607173..a84ce2333f 100644
--- a/library/init/meta/has_reflect.lean
+++ b/library/init/meta/has_reflect.lean
@@ -16,8 +16,8 @@ section
 local attribute [semireducible] reflected
 
 meta instance nat.reflect : has_reflect ℕ
-| n := if n = 0 then `(nat.zero)
-       else if n = 1 then `(1 : nat)
+| n := if n = 0 then `(0 : ℕ)
+       else if n = 1 then `(1 : ℕ)
        else if n % 2 = 0 then `(bit0 %%(nat.reflect (n / 2)) : ℕ)
        else `(bit1 %%(nat.reflect (n / 2)) : ℕ)
 
@@ -48,3 +48,10 @@ meta instance prod.reflect {α β : Type} [has_reflect α] [reflected α] [has_r
 
 meta instance pos.reflect : has_reflect pos
 | ⟨l, c⟩ := `(_)
+
+meta def reflect_to_format {α} {a : α} (h : reflected a) : format :=
+to_fmt (reflect a).to_expr
+
+meta instance reflected.has_to_format {α} (a : α) : has_to_format (reflected a) :=
+⟨reflect_to_format⟩
+
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index fa8709962d..aa4b53efd8 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -189,6 +189,12 @@ meta def option_to_tactic_format {α : Type u} [has_to_tactic_format α] : optio
 meta instance {α : Type u} [has_to_tactic_format α] : has_to_tactic_format (option α) :=
 ⟨option_to_tactic_format⟩
 
+meta def reflect_to_tactic_format {α} {a : α} (h : reflected a) : tactic format :=
+pp (reflect a).to_expr
+
+meta instance reflected.has_to_tactic_format {α} (a : α) : has_to_tactic_format (reflected a) :=
+⟨reflect_to_tactic_format⟩
+
 @[priority 10] meta instance has_to_format_to_has_to_tactic_format (α : Type) [has_to_format α] : has_to_tactic_format α :=
 ⟨(λ x, return x) ∘ to_fmt⟩