diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index f44210053a..3258418f20 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -305,6 +305,8 @@ macro_rules let r ← Lean.Syntax.expandInterpolatedStrChunks chunks (fun a b => `($a ++ $b)) (fun a => `(toMessageData $a)) `(($r : MessageData)) +-- TODO: interpreter should not compiled code when building stdlib. +-- The following instances cannot be defined before `syntax` because it would change the internal syntax node kinds and break the build. instance {α} [ToMessageData α] : ToMessageData (Option α) := ⟨fun | none => "none" | some e => "some ({toMessageData e})"⟩ instance : ToMessageData (Option Expr) := ⟨fun | none => "" | some e => toMessageData e⟩