Digraph Darts port from simple graph

Stream: mathlib4

[Jafar Tanoukhi]

Does it make sense to define a Dart type for digraphs? Technically, the set of darts of a digraph is also the set of edges, right?

I'm asking because while porting other files like Walk.lean, there are a lot of theorems that reference G.Dart or something similar. Should I just go ahead and port Dart.lean, or should I modify the theorems to work with any edge of a digraph instead?
/user_uploads/3121/b0Mn1bGBC2Ng1Ts4PSbkfSHh/f5f2d82a-17c5-4f04-b98f-dbb730d5604e.jpg
(G here is supposed to be a Digraph)

Here's one example
I think I will need to define G.edgeset or something if I don't want to use darts, tho I'm not sure