Commit 2025-03-12 22:42 2a1697d7
View on Github →chore(Data/(D)Finsupp): clean up porting notes (#22879)
The main issue that remains is #12129: when defining structure fields, the constructor of the parent structure is not reduced away. So we need to first run dsimp/beta_reduce or add type ascriptions.