From b8e5de2fb7f23025b59e4e8b4bfb14520f79a41b Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Wed, 7 Jun 2017 17:22:11 -0400 Subject: [PATCH] fix(reflect): change names --- library/init/meta/has_reflect.lean | 7 +++---- library/init/meta/tactic.lean | 6 +++--- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/library/init/meta/has_reflect.lean b/library/init/meta/has_reflect.lean index a84ce2333f..bbeb076f1a 100644 --- a/library/init/meta/has_reflect.lean +++ b/library/init/meta/has_reflect.lean @@ -49,9 +49,8 @@ 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 := +meta def reflected.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⟩ - +meta instance {α} (a : α) : has_to_format (reflected a) := +⟨reflected.to_format⟩ diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index aa4b53efd8..fb14d07f54 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -189,11 +189,11 @@ 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 := +meta def reflected.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⟩ +meta instance {α} (a : α) : has_to_tactic_format (reflected a) := +⟨reflected.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⟩