From 69ed20f6563d202a68d142e5da456a58fe0b07d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= <johannes.hoelzl@gmx.de>
Date: Mon, 20 Feb 2017 11:12:11 -0500
Subject: [PATCH] feat(library/init/meta/match_tactic): add tactic_format for
 pattern

---
 library/init/meta/match_tactic.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/library/init/meta/match_tactic.lean b/library/init/meta/match_tactic.lean
index b6e5c31b28..a79d0e386e 100644
--- a/library/init/meta/match_tactic.lean
+++ b/library/init/meta/match_tactic.lean
@@ -103,4 +103,13 @@ do ctx ← local_context,
    new_p ← pexpr_to_pattern p,
    match_hypothesis_core new_p ctx
 
+meta instance : has_to_tactic_format pattern :=
+⟨λp, do
+  t ← pp p^.target,
+  mo ← pp p^.moutput,
+  uo ← pp p^.uoutput,
+  u ← pp p^.nuvars,
+  m ← pp p^.nmvars,
+  return $ to_fmt "pattern.mk (" ++ t ++ ") " ++ uo ++ " " ++ mo ++ " " ++ u ++ " " ++ m ++ "" ⟩
+
 end tactic