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

fix: error message

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-23 07:35:12 -08:00
parent 9c47cfe001
commit 7e76446d9d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Message.lean
View file

@ -274,7 +274,7 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData :=
| alreadyDeclared env constName => mkCtx env {} opts m!"(kernel) constant has already been declared '{constName}'"
| declTypeMismatch env decl givenType =>
let process (n : Name) (expectedType : Expr) : MessageData :=
m!"(kernel) declaration type mismatch, '{n}' has type{indentExpr givenType}\n, but it is expected to have type{indentExpr expectedType}";
m!"(kernel) declaration type mismatch, '{n}' has type{indentExpr givenType}\nbut it is expected to have type{indentExpr expectedType}";
match decl with
| Declaration.defnDecl { name := n, type := type, .. } => process n type
| Declaration.thmDecl { name := n, type := type, .. } => process n type