From f7d63c04535f2f258c235220e23ec08de535a0a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 Nov 2019 10:40:39 -0800
Subject: [PATCH] chore: improve `Array Expr` to `MessageData` coercion

---
 library/Init/Lean/Message.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/library/Init/Lean/Message.lean b/library/Init/Lean/Message.lean
index 14a181a434..0f2be1e2c4 100644
--- a/library/Init/Lean/Message.lean
+++ b/library/Init/Lean/Message.lean
@@ -65,7 +65,17 @@ instance coeOfFormat    : HasCoe Format MessageData := ⟨ofFormat⟩
 instance coeOfLevel     : HasCoe Level MessageData := ⟨ofLevel⟩
 instance coeOfExpr      : HasCoe Expr MessageData := ⟨ofExpr⟩
 instance coeOfName      : HasCoe Name MessageData := ⟨ofName⟩
-instance coeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => node $ es.map $ fun e => ofExpr e⟩
+
+partial def arrayExpr.toMessageData (es : Array Expr) : Nat → MessageData → MessageData
+| i, acc =>
+  if h : i < es.size then
+    let e   := es.get ⟨i, h⟩;
+    let acc := if i == 0 then acc ++ ofExpr e else acc ++ ", " ++ ofExpr e;
+    arrayExpr.toMessageData (i+1) acc
+  else
+    acc ++ "]"
+
+instance coeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
 
 end MessageData