Parameters across files

Stream: general

[Alistair Tucker]

I have been assuming a couple of functions with various properties that I put down as parameters at the top of my file. But now I want to break this file up into several pieces (hoping then edits will be more easily processed by my near-decade-old computer). Now it seems I need to pass a lot of extra arguments when using definitions and results in one file from another. Is there some way around this?

[Alistair Tucker]

In theory I could define these functions and prove their properties but it would probably take months to do.

[Yury G. Kudryashov]

parameters will go away in Lean 4. We try to use variables.

[Yury G. Kudryashov]

If you have the same long list of arguments to many definitions/lemmas, then you can define a structure.

[Utensil Song]

Yury G. Kudryashov said:

parameters will go away in Lean 4. We try to use variables.

Oh no, then my problem here (which was solved by replacing variables to parameters) is again a serious problem...