RFC: attribute induction_case_names
@nomeata is already working on this.
Since Feb 4, 2025.
- Dominant language
- Lean
- Stars
- 9.2k
- Forks
- 990
- Avg merge
- 1d 17h
- Merged PRs (30d)
- 175
Description
Proposal
Now that users are reporting success stories about the functional induction principle, they rightfully are not amused by the unhelpful naming of the cases (case1, case2, etc.).
What one probably really wants is a way to annotate the corresponding branches directly in the function definition, possibly with a generic “label” mechanism. But that’s not easy to design nicely.
A decent half-way solution that helps at least when one plans to use a function’s induction principle a lot would be an attribute like @[induction_case_names nil cons_pos cons_neg] that just labels the cases. A bit fragile when the function (or the induction principle generation) changes, but overall a probably helpful addition.
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.