From 9098cb0eab6951ae67c87549facb48e563cd3ec0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2019 11:00:27 -0800 Subject: [PATCH] chore: add trace message for typing errors --- library/Init/Lean/Meta/ExprDefEq.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/Init/Lean/Meta/ExprDefEq.lean b/library/Init/Lean/Meta/ExprDefEq.lean index 7f7a0b0181..4388e0b193 100644 --- a/library/Init/Lean/Meta/ExprDefEq.lean +++ b/library/Init/Lean/Meta/ExprDefEq.lean @@ -678,7 +678,8 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) a type incorrect term. See discussion at A2 -/ condM (isTypeCorrect v) (finalize ()) - (useFOApprox ()) + (do trace! `Meta.isDefEq.assignment.typeError (mvar ++ " := " ++ v); + useFOApprox ()) else finalize ()