From 14e626a925397f3bb98df071d127b5e2cd2d3b8b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 11 Oct 2023 00:26:31 -0400 Subject: [PATCH] =?UTF-8?q?feat:=20ToMessageData=20(=CE=B1=20=C3=97=20?= =?UTF-8?q?=CE=B2)=20instance?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Lean/Message.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index d2dc1b0434..cfb3508279 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -328,6 +328,8 @@ instance [ToMessageData α] : ToMessageData (List α) := ⟨fun as => MessageDa instance [ToMessageData α] : ToMessageData (Array α) := ⟨fun as => toMessageData as.toList⟩ instance [ToMessageData α] : ToMessageData (Subarray α) := ⟨fun as => toMessageData as.toArray.toList⟩ instance [ToMessageData α] : ToMessageData (Option α) := ⟨fun | none => "none" | some e => "some (" ++ toMessageData e ++ ")"⟩ +instance [ToMessageData α] [ToMessageData β] : ToMessageData (α × β) := + ⟨fun (a, b) => .paren <| toMessageData a ++ "," ++ Format.line ++ toMessageData b⟩ instance : ToMessageData (Option Expr) := ⟨fun | none => "" | some e => toMessageData e⟩ syntax:max "m!" interpolatedStr(term) : term