diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean
index 363883db25..7a211c461a 100644
--- a/library/init/lean/parser/basic.lean
+++ b/library/init/lean/parser/basic.lean
@@ -9,6 +9,7 @@ prelude
 import init.lean.parser.parsec init.lean.parser.syntax init.lean.parser.rec
 import init.lean.parser.trie
 import init.lean.parser.identifier init.data.rbmap init.lean.message
+import init.control.coroutine
 
 namespace lean
 namespace parser
diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean
index f711bffde7..8fd12fc75c 100644
--- a/library/init/lean/parser/combinators.lean
+++ b/library/init/lean/parser/combinators.lean
@@ -7,6 +7,7 @@ Syntax-tree creating parser combinators
 -/
 prelude
 import init.lean.parser.basic
+import init.data.list.instances
 
 namespace lean
 namespace parser
diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean
index b2034fcd98..767e0860b4 100644
--- a/library/init/lean/parser/trie.lean
+++ b/library/init/lean/parser/trie.lean
@@ -5,7 +5,12 @@ Author: Sebastian Ullrich
 
 Trie for tokenizing the Lean language
 -/
-namespace lean.parser
+prelude
+import init.data.rbmap
+import init.lean.format
+
+namespace lean
+namespace parser
 
 inductive trie (α : Type)
 | node : option α → rbnode (char × trie) → trie
@@ -44,6 +49,14 @@ private def match_prefix_aux : nat → trie α → string.iterator → option (s
 
 def match_prefix {α : Type} (t : trie α) (it : string.iterator) : option (string.iterator × α) :=
 match_prefix_aux it.remaining t it none
+
+private def to_string_aux {α : Type} : trie α → list format
+| (trie.node val map) := flip rbnode.fold map (λ ⟨c, t⟩ fs,
+  to_format (repr c) :: (format.group $ format.nest 2 $ flip format.join_sep format.line $ to_string_aux t) :: fs) []
+
+instance {α : Type} : has_to_string (trie α) :=
+⟨λ t, (flip format.join_sep format.line $ to_string_aux t).pretty 0⟩
 end trie
 
-end lean.parser
+end parser
+end lean