mkCommDiag

Mathlib.Tactic.Widget.CommDiag

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

Lean4

/-- Construct a commutative diagram from a Penrose `sub`stance program and expressions `embeds` to
display as labels in the diagram. -/
def mkCommDiag (sub : String) (embeds : ExprEmbeds) : MetaM Html := do
  let embeds ← embeds.mapM fun (s, h) => return (s, <InteractiveCode fmt={← Widget.ppExprTagged h}/>)
  return
    (<PenroseDiagram
        embeds={embeds}dsl={include_str
              ".." / ".." / ".." / "widget" / "src" / "penrose" /
                "commutative.dsl"}sty={include_str
              ".." / ".." / ".." / "widget" / "src" / "penrose" / "commutative.sty"}sub={sub}/>)

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

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

Разделы

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

Аффилиация

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