max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: Option.ToMessageData

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-27 11:13:15 +01:00
parent 5f67c359bc
commit c0e117daa4
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Message.lean
View file

@ -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 => "<not-available>" | some e => toMessageData e⟩
syntax:max "msg!" (interpolatedStr term) : term