StringDiagram
📁 Source: Mathlib/Tactic/Widget/StringDiagram.lean
Statistics
| Metric | Count |
|---|---|
Definitionsnodes, nodes, nodesAux, strands, nodes, nodes, pairs, topNodes, StringDiagram, AtomNode, atom, hPosSrc, hPosTar, vPos, IdNode, hPosSrc, hPosTar, id, vPos, Kind, name, Node, e, hPosSrc, hPosTar, srcList, tarList, toPenroseVar, vPos, PenroseVar, e, ident, indices, Strand, atom₁, endPoint, hPos, startPoint, toPenroseVar, vPos, addConstructor, addPenroseVar, dsl, instToStringPenroseVar, mkEqHtml, mkKind, mkStringDiagram, rpc, stringEqM?, stringM?, stringMorOrEqM?, stringPresenter, sty, elabStringDiagramCmd, stringDiagram | 55 |
| Theorems | 0 |
| Total | 55 |
Mathlib.Tactic.BicategoryLike
Definitions
| Name | Category | Theorems |
|---|---|---|
pairs 📖 | CompOp | — |
topNodes 📖 | CompOp | — |
Mathlib.Tactic.BicategoryLike.HorizontalComp
Definitions
| Name | Category | Theorems |
|---|---|---|
nodes 📖 | CompOp | — |
Mathlib.Tactic.BicategoryLike.NormalExpr
Definitions
| Name | Category | Theorems |
|---|---|---|
nodes 📖 | CompOp | — |
nodesAux 📖 | CompOp | — |
strands 📖 | CompOp | — |
Mathlib.Tactic.BicategoryLike.WhiskerLeft
Definitions
| Name | Category | Theorems |
|---|---|---|
nodes 📖 | CompOp | — |
Mathlib.Tactic.BicategoryLike.WhiskerRight
Definitions
| Name | Category | Theorems |
|---|---|---|
nodes 📖 | CompOp | — |
Mathlib.Tactic.Widget
Definitions
| Name | Category | Theorems |
|---|---|---|
StringDiagram 📖 | CompOp | — |
elabStringDiagramCmd 📖 | CompOp | — |
stringDiagram 📖 | CompOp | — |
Mathlib.Tactic.Widget.StringDiagram
Definitions
| Name | Category | Theorems |
|---|---|---|
AtomNode 📖 | CompData | — |
IdNode 📖 | CompData | — |
Kind 📖 | CompData | — |
Node 📖 | CompData | — |
PenroseVar 📖 | CompData | — |
Strand 📖 | CompData | — |
addConstructor 📖 | CompOp | — |
addPenroseVar 📖 | CompOp | — |
dsl 📖 | CompOp | — |
instToStringPenroseVar 📖 | CompOp | — |
mkEqHtml 📖 | CompOp | — |
mkKind 📖 | CompOp | — |
mkStringDiagram 📖 | CompOp | — |
rpc 📖 | CompOp | — |
stringEqM? 📖 | CompOp | — |
stringM? 📖 | CompOp | — |
stringMorOrEqM? 📖 | CompOp | — |
stringPresenter 📖 | CompOp | — |
sty 📖 | CompOp | — |
Mathlib.Tactic.Widget.StringDiagram.AtomNode
Definitions
| Name | Category | Theorems |
|---|---|---|
atom 📖 | CompOp | — |
hPosSrc 📖 | CompOp | — |
hPosTar 📖 | CompOp | — |
vPos 📖 | CompOp | — |
Mathlib.Tactic.Widget.StringDiagram.IdNode
Definitions
| Name | Category | Theorems |
|---|---|---|
hPosSrc 📖 | CompOp | — |
hPosTar 📖 | CompOp | — |
id 📖 | CompOp | — |
vPos 📖 | CompOp | — |
Mathlib.Tactic.Widget.StringDiagram.Kind
Definitions
| Name | Category | Theorems |
|---|---|---|
name 📖 | CompOp | — |
Mathlib.Tactic.Widget.StringDiagram.Node
Definitions
| Name | Category | Theorems |
|---|---|---|
e 📖 | CompOp | — |
hPosSrc 📖 | CompOp | — |
hPosTar 📖 | CompOp | — |
srcList 📖 | CompOp | — |
tarList 📖 | CompOp | — |
toPenroseVar 📖 | CompOp | — |
vPos 📖 | CompOp | — |
Mathlib.Tactic.Widget.StringDiagram.PenroseVar
Definitions
| Name | Category | Theorems |
|---|---|---|
e 📖 | CompOp | — |
ident 📖 | CompOp | — |
indices 📖 | CompOp | — |
Mathlib.Tactic.Widget.StringDiagram.Strand
Definitions
| Name | Category | Theorems |
|---|---|---|
atom₁ 📖 | CompOp | — |
endPoint 📖 | CompOp | — |
hPos 📖 | CompOp | — |
startPoint 📖 | CompOp | — |
toPenroseVar 📖 | CompOp | — |
vPos 📖 | CompOp | — |
---