From 6b318ddde6675404c367cb5484e346dc84cd75d0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Jul 2022 12:24:36 -0700 Subject: [PATCH] chore: style --- src/Lean/Message.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index e061bac4e2..4ecba79837 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -288,7 +288,7 @@ def stringToMessageData (str : String) : MessageData := let lines := lines.map (MessageData.ofFormat ∘ format) MessageData.joinSep lines (MessageData.ofFormat Format.line) -instance {α} [ToFormat α] : ToMessageData α := ⟨MessageData.ofFormat ∘ format⟩ +instance [ToFormat α] : ToMessageData α := ⟨MessageData.ofFormat ∘ format⟩ instance : ToMessageData Expr := ⟨MessageData.ofExpr⟩ instance : ToMessageData Level := ⟨MessageData.ofLevel⟩ instance : ToMessageData Name := ⟨MessageData.ofName⟩ @@ -298,10 +298,10 @@ instance : ToMessageData (TSyntax k) := ⟨(MessageData.ofSyntax ·)⟩ instance : ToMessageData Format := ⟨MessageData.ofFormat⟩ instance : ToMessageData MVarId := ⟨MessageData.ofGoal⟩ instance : ToMessageData MessageData := ⟨id⟩ -instance {α} [ToMessageData α] : ToMessageData (List α) := ⟨fun as => MessageData.ofList <| as.map toMessageData⟩ -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 (List α) := ⟨fun as => MessageData.ofList <| as.map toMessageData⟩ +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 (Option Expr) := ⟨fun | none => "" | some e => toMessageData e⟩ syntax:max "m!" interpolatedStr(term) : term