From bdf89b4d856c3e8edf85668c375dd631d2caaf82 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 27 Aug 2022 07:35:57 -0700
Subject: [PATCH] chore: add `{crossEmoji}` at failure

---
 src/Lean/Meta/SynthInstance.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index bf5a850873..4a3c2be27d 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -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?