Additional operations on MessageData and related types

instance instToMessageDataProd {α : Type} {β : Type} [Lean.ToMessageData α] [Lean.ToMessageData β] : Lean.ToMessageData (α × β)

Equations

• One or more equations did not get rendered due to their size.