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