From a225bac3df8f5616d9ff7bd3cb63f5c78c32b510 Mon Sep 17 00:00:00 2001 From: Jannis Limperg Date: Tue, 12 May 2020 16:33:12 +0200 Subject: [PATCH] =?UTF-8?q?feat(library/init/meta/format):=20has=5Fto=5Ffo?= =?UTF-8?q?rmat=20=CE=B1=20implies=20has=5Fto=5Fstring=20=CE=B1?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This commit adds a low-priority meta instance which concludes `has_to_string α` from `has_to_format α`. The instance has to be meta since `format` is meta. This means that for most types, it is still preferable to give a non-meta `has_to_string` instance manually. --- library/init/meta/format.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean index d29d279943..3dc2c8e0c9 100644 --- a/library/init/meta/format.lean +++ b/library/init/meta/format.lean @@ -53,7 +53,7 @@ meta instance : has_append format := ⟨format.compose⟩ meta instance : has_to_string format := -⟨λ f, f.to_string options.mk⟩ +⟨λ f, f.to_string⟩ /-- Use this instead of `has_to_string` to enable prettier formatting. See docstring for `format` for more on the differences between `format` and `string`. @@ -61,6 +61,10 @@ Note that `format` is `meta` while `string` is not. -/ meta class has_to_format (α : Type u) := (to_format : α → format) +@[priority 10] meta instance has_to_format_has_to_string {α} [has_to_format α] + : has_to_string α := +⟨has_to_string.to_string ∘ has_to_format.to_format⟩ + meta instance : has_to_format format := ⟨id⟩