Stream: general

Topic: Where to cut this import chain

Eric Wieser (Dec 02 2020 at 20:15):

Items at the start of the list are imported by items at the end ofthe list:

['group_theory.perm.basic',
'deprecated.group',
'algebra.group_power.basic',
'data.nat.basic',
'data.nat.factorial',
'data.list.perm',
'tactic.wlog',
'data.fintype.basic']


I want to import data.fintype.basic in group_theory.perm.basic, but I can't right now.

Johan Commelin (Dec 02 2020 at 20:20):

Maybe data.fintype.basic is too basic to use wlog?

Johan Commelin (Dec 02 2020 at 20:20):

But also wlog seems to have pretty heavy imports... otoh, I understand that it might want to know something about permutations.

Johan Commelin (Dec 02 2020 at 20:21):

But having tactic.wlog import all that seems quite much. I wonder if we can minimize something there.

Eric Wieser (Dec 02 2020 at 20:21):

Cutting deprecated.group out shouldn't be too hard

Eric Wieser (Dec 02 2020 at 20:22):

Although I suspec the cycle reappears somewhere else

Rob Lewis (Dec 02 2020 at 20:23):

wlog is used exactly once in fintype.basic so that would be an easy cut.

Rob Lewis (Dec 02 2020 at 20:23):

But also permutations in nat.basic seems a little much, no?

Eric Wieser (Dec 02 2020 at 20:30):

I think I'll try swapping the import direction between group_power.basic and deprecated.group

#5194

Eric Wieser (Dec 03 2020 at 10:33):

Reid Barton said:

For now, the fintype import is in equiv.perm.sign instead, #5201
I cut the import of perm.basic from mul_add in #5281 - which was enough to show me that perm.basic is used by fintype.basic directly anyway, making the rest of the import chain irrelevant.