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

feat: ToMessageData (α × β) instance

Browse source
This commit is contained in:
Mario Carneiro 2023-10-11 00:26:31 -04:00 • committed by Sebastian Ullrich
parent 856a9b5153
commit 14e626a925
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Message.lean
View file

@ -328,6 +328,8 @@ instance [ToMessageData α] : ToMessageData (List α) := ⟨fun as => MessageDa
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 β] : ToMessageData (α × β) :=
⟨fun (a, b) => .paren <| toMessageData a ++ "," ++ Format.line ++ toMessageData b⟩
instance : ToMessageData (Option Expr) := ⟨fun | none => "<not-available>" | some e => toMessageData e⟩
syntax:max "m!" interpolatedStr(term) : term