diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index d415b86412..70e6cd0e27 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -178,4 +178,18 @@ private def withNestedTracesFinalizer [Monad m] [MonadTrace m] (ref : Syntax) (c
   let ref ← getRef
   try x finally withNestedTracesFinalizer ref currTraces
 
+def bombEmoji := "💥"
+def checkEmoji := "✅"
+def crossEmoji := "❌"
+
+def exceptBoolEmoji : Except ε Bool → String
+  | .error _ => bombEmoji
+  | .ok true => checkEmoji
+  | .ok false => crossEmoji
+
+def exceptOptionEmoji : Except ε (Option α) → String
+  | .error _ => bombEmoji
+  | .ok (some _) => checkEmoji
+  | .ok none => crossEmoji
+
 end Lean