From 669f8fc9df220a2bc40a3a1468d8b7798eaace26 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jun 2016 14:34:55 +0100 Subject: [PATCH] feat(library/init/meta/tactic): make sure to_format ==> to_tactic_format has higher priority --- library/init/meta/tactic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index d5eac4a0cc..5acfab9ea1 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -31,9 +31,6 @@ do s ← tactic.read, return (tactic_state.format_expr s e) structure has_to_tactic_format [class] (A : Type) := (to_tactic_format : A → tactic format) -meta_definition has_to_format_to_has_to_tactic_format [instance] (A : Type) [has_to_format A] : has_to_tactic_format A := -has_to_tactic_format.mk (return ∘ to_fmt) - meta_definition expr_has_to_tactic_format [instance] : has_to_tactic_format expr := has_to_tactic_format.mk tactic.format_expr @@ -58,6 +55,9 @@ meta_definition list_to_tactic_format {A : Type} [has_to_tactic_format A] : list meta_definition list_has_to_tactic_format [instance] {A : Type} [has_to_tactic_format A] : has_to_tactic_format (list A) := has_to_tactic_format.mk list_to_tactic_format +meta_definition has_to_format_to_has_to_tactic_format [instance] (A : Type) [has_to_format A] : has_to_tactic_format A := +has_to_tactic_format.mk (return ∘ to_fmt) + namespace tactic open tactic_state