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

fix: missing line breaks

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-24 11:18:28 -07:00
parent 302ff1b10e
commit 20210928da
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Message.lean
View file

@ -207,8 +207,8 @@ match e with
| appTypeMismatch env lctx e fnType argType =>
mkCtx env lctx opts $
"application type mismatch" ++ indentExpr e
++ "argument has type" ++ indentExpr argType
++ "but function has type" ++ indentExpr fnType
++ Format.line ++ "argument has type" ++ indentExpr argType
++ Format.line ++ "but function has type" ++ indentExpr fnType
| invalidProj env lctx e => mkCtx env lctx opts $ "(kernel) invalid projection" ++ indentExpr e
| other msg => "(kernel) " ++ msg