max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/lean/parser/parser): missing space

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-16 13:10:07 -07:00
parent 8a11c8509e
commit a52f67cea8
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/parser/parser.lean
View file

@ -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⟩