Directed (flow) graphs and dominator trees?

Stream: Is there code for X?

[Siddharth Bhat]

I'm interested in slowly verifying key properties relating to dominance on a flow graph. I was unable to find directed graphs in mathlib, but I guess one can squint at a quiver and (ab)use it to represent directed graphs. Is this the recommended path?

[Siddharth Bhat]

To be clear, I'm interested in developing the theory such that there's a chance it's upstreamable, so I would like to at least pick the mathlib-style representation if nothing else!

[Siddharth Bhat]

(CC @Tobias Grosser @Andrés Goens @Alex Keizer )

[Daniel Weber]

You might also want to ask in #graph theory . Anyway as far as I know directed graphs aren't in Mathlib yet, and I'm not sure what's the current plan for adding them

[Shreyas Srinivas]

There is a PR on the #queue that adds the basic defs of a directed graph