nodes

Mathlib.Tactic.Widget.StringDiagram

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.BicategoryLike.NormalExpr.nodes

Lean4

/-- The list of nodes associated with a 2-morphism. -/
def nodes (e : NormalExpr) : CoherenceM ρ (List (List Node)) :=
  match e with
  | NormalExpr.nil _ _ => return []
  | NormalExpr.cons _ _ η _ => return (← topNodes η) :: (← e.nodesAux 1)

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

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

Разделы

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

Аффилиация

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