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

chore: style

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-29 12:24:36 -07:00
parent 3362b38829
commit 6b318ddde6
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Message.lean
View file

@ -288,7 +288,7 @@ def stringToMessageData (str : String) : MessageData :=
let lines := lines.map (MessageData.ofFormat ∘ format)
MessageData.joinSep lines (MessageData.ofFormat Format.line)
instance {α} [ToFormat α] : ToMessageData α := ⟨MessageData.ofFormat ∘ format⟩
instance [ToFormat α] : ToMessageData α := ⟨MessageData.ofFormat ∘ format⟩
instance : ToMessageData Expr := ⟨MessageData.ofExpr⟩
instance : ToMessageData Level := ⟨MessageData.ofLevel⟩
instance : ToMessageData Name := ⟨MessageData.ofName⟩
@ -298,10 +298,10 @@ instance : ToMessageData (TSyntax k) := ⟨(MessageData.ofSyntax ·)⟩
instance : ToMessageData Format := ⟨MessageData.ofFormat⟩
instance : ToMessageData MVarId := ⟨MessageData.ofGoal⟩
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 (Subarray α) := ⟨fun as => toMessageData as.toArray.toList⟩
instance {α} [ToMessageData α] : ToMessageData (Option α) := ⟨fun | none => "none" | some e => "some (" ++ toMessageData e ++ ")"⟩
instance [ToMessageData α] : ToMessageData (List α) := ⟨fun as => MessageData.ofList <| as.map toMessageData⟩
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 (Option Expr) := ⟨fun | none => "<not-available>" | some e => toMessageData e⟩
syntax:max "m!" interpolatedStr(term) : term