chore: document temporary workaround

This commit is contained in:
Leonardo de Moura 2020-10-18 12:22:20 -07:00
parent a9d2620a6c
commit bc072eceea

View file

@ -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 => "<not-available>" | some e => toMessageData e⟩