Proposal to separate elaboration from adding declarations

Stream: lean4

[Alex Keizer]

Would the team be open to a PR that separates mkInductiveDecl (from Lean/Elab/Inductive.lean) into two functions:
One that does all type elaboration related work, without modifying the environment, rather, returning some InductiveDecl struct that takes the same argument as Declaration.inductDecl currently does,
and a second function which calls addDecl and mkAuxConstructions and other environment-modifying stuff. (or even just move these calls to elabInductiveViews).

My motivation is that I'm working on my own inductive datatype macro, which is based on alternative constructions (qpfs). Still, I want it to be a drop-in replacement with the same syntax and elaboration behavior. I started by copying mkInductiveDecl and removing the side-effecting behaviour, but it calls a lot of private functions which I then had to copy as well, resulting in a maintenance nightmare.

[Alex Keizer]

@Leonardo de Moura could you comment on this? Since it's a relatively minor change I'll go ahead and implement it, but feel free to stop me

[Leonardo de Moura]

@Alex Keizer This is a reasonable suggestion.
We want to make the first Lean 4 official release this summer, and we are currently trying to focus on bugs and missing features. Reviewing PRs consumes time, and we are trying to focus on PRs that will benefit the whole community (e.g., widget related).
What about the following compromise?

• Keep your changes to Inductive.lean in your own private branch for now. We are not planning to make any substantial changes to Inductive.lean.
• After you finish the alternative construction (qpfs), and it is useful to the community, we work to get your changes to Inductive.lean merged into the main repo.

[Alex Keizer]

Your compromise seems entirely fair, thanks for taking the time to respond.

[Marcus Rossel]

@Alex Keizer This sounds exciting! Would your QPF implementation give us coinductive types?

[Alex Keizer]

Yes! That's the eventual goal.