stringPresenter

Mathlib.Tactic.Widget.StringDiagram

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Widget.StringDiagram.stringPresenter

Lean4

/-- The `Expr` presenter for displaying string diagrams. -/
@[expr_presenter]
def stringPresenter : ExprPresenter where
  userName := "String diagram"
  layoutKind := .block
  present
    type := do
    if let some html← stringMorOrEqM? type then
      return html
    throwError"Couldn't find a 2-morphism to display a string diagram."

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

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

Разделы

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

Аффилиация

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