Question on the implementation of intersect

[ionchirica]

Dear OCamlGraph developers,

This is not really an issue, but rather a question about implementation choices.

Together with @mariojppereira, we have an ongoing project of formally verifying parts of the OCamlGraph library, using the Cameleer tool.

We have stumbled upon oper.ml's intersect when trying to prove it. I am wondering on why it uses List.exists (fun e' -> G.E.compare e e' = 0) succ to test the membership of an edge e in successors succ. Wouldn't something along the lines of G.mem_edge_e e g2 be equivalent - with the benefit of using O(log n) lookup instead of O(n) that comes from List.exists?

Thank you,
Ion.

[backtracking]

Hi @ionchirica ,
Apologies for the late reply. Indeed, I see no good reason for not using G.mem_edge_e here.