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

chore: add {crossEmoji} at failure

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-27 07:35:57 -07:00
parent 48c1ddc807
commit bdf89b4d85
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/Meta/SynthInstance.lean
View file

@ -722,7 +722,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
check result
pure (some result)
else
trace[Meta.synthInstance] "result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
trace[Meta.synthInstance] "{crossEmoji} result type{indentExpr resultType}\nis not definitionally equal to{indentExpr type}"
pure none
if type.hasMVar || resultHasUnivMVars then
pure result?