Zulip Chat Archive

Stream: general

Topic: Parameters across files


Alistair Tucker (Jun 17 2020 at 11:18):

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 (Jun 17 2020 at 11:20):

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

Yury G. Kudryashov (Jun 17 2020 at 13:08):

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

Yury G. Kudryashov (Jun 17 2020 at 13:08):

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

Utensil Song (Jun 17 2020 at 14:46):

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...


Last updated: Dec 20 2023 at 11:08 UTC