Additional operations on MessageData and related types

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

Equations

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