Additional operations on MessageData and related types #
instance
instToMessageDataProd_mathlib
{α : Type}
{β : Type}
[Lean.ToMessageData α]
[Lean.ToMessageData β]
:
Lean.ToMessageData (α × β)
Equations
- One or more equations did not get rendered due to their size.