diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 485b9dce1f..269ceb63de 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -287,7 +287,7 @@ instance : ToMessageData Format := ⟨MessageData.ofFormat⟩ 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 (Option α) := ⟨fun | none => "none" | some e => "some ({toMessageData e})"⟩ +instance {α} [ToMessageData α] : ToMessageData (Option α) := ⟨fun | none => "none" | some e => "some (" ++ toMessageData e ++ ")"⟩ instance : ToMessageData (Option Expr) := ⟨fun | none => "" | some e => toMessageData e⟩ syntax:max "msg!" (interpolatedStr term) : term