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

chore: add trace message for typing errors

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-21 11:00:27 -08:00
parent 21f37e7f6a
commit 9098cb0eab
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/Init/Lean/Meta/ExprDefEq.lean
View file

@ -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 ()