def Duper.ExprPairToMessageData : Lean.Expr × Lean.Expr → Lean.MessageData

Equations

• Duper.ExprPairToMessageData (e1, e2) = (Lean.toMessageData "(" ++ Lean.toMessageData e1 ++ Lean.toMessageData ", ").compose (Lean.toMessageData e2 ++ Lean.toMessageData ")")

def Duper.ListToMessageData {α : Type u_1} (as : List α) (f : α → Lean.MessageData) : Lean.MessageData

Equations

• Duper.ListToMessageData as f = (Lean.toMessageData "[").compose ((Duper.ListToMessageData.go f as).compose (Lean.toMessageData "]"))

@[irreducible]

def Duper.ListToMessageData.go {α : Type u_1} (f : α → Lean.MessageData) (as : List α) : Lean.MessageData

Equations

• Duper.ListToMessageData.go f [] = Lean.toMessageData ""
• Duper.ListToMessageData.go f [a] = f a
• Duper.ListToMessageData.go f (a :: head :: tail) = (f a).compose (((Lean.MessageData.ofFormat ∘ Std.format) ", ").compose (Duper.ListToMessageData.go f (head :: tail)))

def Duper.ArrayToMessageData {α : Type u_1} (as : Array α) (f : α → Lean.MessageData) : Lean.MessageData

Equations

• Duper.ArrayToMessageData as f = Duper.ListToMessageData as.toList f