Gmap.Edge
Provide a mapping function from a mapping of edges.
val map : ( G_Src.E.t -> G_Dst.edge ) -> G_Src.t -> G_Dst.t
map f g
applies f
to each edge of g
and so builds a new graph based on g
val filter_map : ( G_Src.E.t -> G_Dst.edge option ) -> G_Src.t -> G_Dst.t
filter_map f g
applies f
to each edge of g
and so builds a new graph based on g
; if None
is returned by f
the edge is omitted in the new graph.