From 7e020d45e69ff3581fa160a5a9388dc619e71daa Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sun, 7 Aug 2022 17:54:10 +0200
Subject: [PATCH] feat: add emoji helpers for trace messages

---
 src/Lean/Util/Trace.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

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