Commit 2024-07-30 17:49 b0a0fca7

View on Github →

feat: string diagram widget (#10581) Add the widget to display string diagram of monoidal category morphism.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/CategoryTheory/Monoidal.lean

deleted def Mathlib.Tactic.Monoidal.mkContext

added def Mathlib.Tactic.Monoidal.mkContext?

Created Mathlib/Tactic/Widget/StringDiagram.lean

added def Mathlib.Tactic.Monoidal.NormalExpr.nodes

added def Mathlib.Tactic.Monoidal.NormalExpr.nodesAux

added def Mathlib.Tactic.Monoidal.NormalExpr.strands

added def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.nodes

added def Mathlib.Tactic.Monoidal.WhiskerRightExpr.nodes

added def Mathlib.Tactic.Monoidal.pairs

added structure Mathlib.Tactic.Widget.StringDiagram.AtomNode

added structure Mathlib.Tactic.Widget.StringDiagram.IdNode

added def Mathlib.Tactic.Widget.StringDiagram.Node.e

added def Mathlib.Tactic.Widget.StringDiagram.Node.hPosSrc

added def Mathlib.Tactic.Widget.StringDiagram.Node.hPosTar

added def Mathlib.Tactic.Widget.StringDiagram.Node.srcList

added def Mathlib.Tactic.Widget.StringDiagram.Node.tarList

added def Mathlib.Tactic.Widget.StringDiagram.Node.toPenroseVar

added def Mathlib.Tactic.Widget.StringDiagram.Node.vPos

added inductive Mathlib.Tactic.Widget.StringDiagram.Node

added structure Mathlib.Tactic.Widget.StringDiagram.PenroseVar

added def Mathlib.Tactic.Widget.StringDiagram.Strand.toPenroseVar

added def Mathlib.Tactic.Widget.StringDiagram.Strand.vPos

added structure Mathlib.Tactic.Widget.StringDiagram.Strand

added def Mathlib.Tactic.Widget.StringDiagram.StringDiagram

added def Mathlib.Tactic.Widget.StringDiagram.addConstructor

added def Mathlib.Tactic.Widget.StringDiagram.addPenroseVar

added def Mathlib.Tactic.Widget.StringDiagram.dsl

added def Mathlib.Tactic.Widget.StringDiagram.fromExpr

added def Mathlib.Tactic.Widget.StringDiagram.mkEqHtml

added def Mathlib.Tactic.Widget.StringDiagram.mkStringDiagram

added def Mathlib.Tactic.Widget.StringDiagram.rpc

added def Mathlib.Tactic.Widget.StringDiagram.stringEqM?

added def Mathlib.Tactic.Widget.StringDiagram.stringM?

added def Mathlib.Tactic.Widget.StringDiagram.stringMorOrEqM?

added def Mathlib.Tactic.Widget.StringDiagram.stringPresenter

added def Mathlib.Tactic.Widget.StringDiagram.sty

added def Mathlib.Tactic.Widget.StringDiagram.topNodes

Modified scripts/noshake.json

Created test/StringDiagram.lean

added theorem left_triangle

added theorem yang_baxter''

added theorem yang_baxter'

added theorem yang_baxter

Created widget/src/penrose/monoidal.dsl

Created widget/src/penrose/monoidal.sty