feat(reflect): add formatting instances and make nat.reflect 0 a numeral

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⟩
+

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⟩