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.