synthMonoidalError

Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Monoidal.synthMonoidalError

Lean4

/-- Throw an error if the monoidal category instance is not found. -/
def synthMonoidalError {α : Type} : MetaM α := do
  throwError"failed to find monoidal category instance"

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru