Documentation
Mathlib
.
Lean
.
Message
Search
Google site search
Mathlib
.
Lean
.
Message
source
Imports
Init
Lean.Message
Imported by
instToMessageDataProd
Additional operations on MessageData and related types
#
source
instance
instToMessageDataProd
{α :
Type
}
{β :
Type
}
[
Lean.ToMessageData
α
]
[
Lean.ToMessageData
β
]
:
Lean.ToMessageData
(
α
×
β
)