From a52f67cea80536ddfbc117a9d45bb3ff08375c8b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Jul 2019 13:10:07 -0700 Subject: [PATCH] chore(library/init/lean/parser/parser): missing space --- library/init/lean/parser/parser.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index db68b20200..392599b26e 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -89,7 +89,7 @@ private def expectedToString : List String → String protected def toString (e : Error) : String := let unexpected := if e.unexpected == "" then [] else ["unexpected " ++ e.unexpected]; let expected := if e.expected == [] then [] else ["expected " ++ expectedToString e.expected]; -";".intercalate $ unexpected ++ expected +"; ".intercalate $ unexpected ++ expected instance : HasToString Error := ⟨Error.toString⟩