mkStringDiagram — Mathlib

Lean4
/-- Construct a string diagram from a Penrose `sub`stance program and expressions `embeds` to
display as labels in the diagram. -/
def mkStringDiagram (nodes : List (List Node)) (strands : List (List Strand)) : DiagramBuilderM PUnit := do
  /- Add 2-morphisms. -/

  for x in nodes.flatten do
    match x with
    | .atom _ =>
      do
        addPenroseVar "Atom" x.toPenroseVar
    | .id _ =>
      do
        addPenroseVar "Id" x.toPenroseVar
  for l in nodes do
    for (x₁, x₂) in pairs l do
      addInstruction s! "Left({x₁.toPenroseVar }, {x₂.toPenroseVar})"
  for (l₁, l₂) in pairs nodes do
    if let some x₁ := l₁.head? then
      if let some x₂ := l₂.head? then
        addInstruction s! "Above({x₁.toPenroseVar }, {x₂.toPenroseVar})"
  for l in strands do
    for s in l do
      addConstructor "Mor1" s.toPenroseVar "MakeString" [s.startPoint.toPenroseVar, s.endPoint.toPenroseVar]
Похожие утверждения