parameters

Stream: general

[Johan Commelin]

Lean 3 had support for parameters. In this message Patrick Massot outlines a way to achieve something similar in Lean 4. Unfortunately it means that statements of intermediate lemmas still mention P. in front of basically everything.

I am curious to hear what other options people have in mind to support long-winded arguments that introduce several intermediate throw-away constructions/definitions/concepts.

[Floris van Doorn]

In the Carleson project I use carleson#ProofData to capture a list of definitions/assumptions common to chapters 4-7 of the blueprint.

1. This is a class, which is keyed by the type X. Most definitions/lemmas already take something related to X as an explicit argument (e.g. (x : X) or (I : Grid X)), and those don't need to take this structure as an additional arguments. Some basic definitions/lemmas that do not depend on X artificially have X as explicit argument to find this class.
2. The class depends on other data other than X, but all of these are out-params (so that they don't need to be know for type-class inference to fire).
3. I also have scoped notation to shorten some common definitions, so that you don't have to write the X explicitly.

This solution works very well in the project.