Zulip Chat Archive

Stream: general

Topic: Import resolution question


view this post on Zulip Chris B (Jul 23 2020 at 03:03):

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)

view this post on Zulip Bryan Gin-ge Chen (Jul 23 2020 at 03:04):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 23 2020 at 03:05):

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

view this post on Zulip Chris B (Jul 23 2020 at 03:10):

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


Last updated: May 09 2021 at 19:11 UTC