Graph

structure Graph : Type :=
(V : ι → Node)
(E : ι → Edge)

structure Edge : Type :=
(v₁ : Node)
(v₂ : Node)
(matched : {0,1})

structure Node : Type :=
(E : ...)

• Graph matching;

• Loopy graphs;