Import resolution question

Stream: general

[Chris B]

Why does #print set.mem_singleton_iffsucceed in a file where the only import statement is import order.complete_lattice? (set.mem_singleton_iff is in data/set/basic.lean)

[Bryan Gin-ge Chen]

data.set.basic is presumably in the transitive imports of order.complete_lattice.

[Bryan Gin-ge Chen]

Here's the output of leanproject import-graph --to order.complete_lattice --from data.set.basic ../imports.png imports.png

[Chris B]

Got it, thanks. I did something wrong when I was trying to figure out the exact behavior of transitive dependencies earlier.