-
Notifications
You must be signed in to change notification settings - Fork 259
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: simps uses fields of parent structures #2042
Conversation
I separated out roughly the definitions you wrote. Thanks for that, they were much nicer than the versions I had myself earlier.
|
It seems like an improvement to me, and given there haven't been any more comments in the last few weeks: bors d+ |
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
* `initialize_simps_projections` now by default generates all projections of all parent structures, and doesn't generate the projections to those parent structures. * You can also rename a nested projection directly, without having to specify intermediate parent structures * Added the option to turn the default behavior off (done in e.g. `TwoPointed`) Internal changes: * Move most declarations to the Simps namespace, and shorten their names * Restructure `ParsedProjectionData` to avoid the bug [reported here](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/allocation.20crash.3F) (and to another bug where it seemed that the wrong data was inserted in `ParsedProjectionData`, but it was hard to minimize because of all the crashes). If we manage to fix the bug in that Zulip thread, I'll see if I can track down the other bug in commit 9745428 Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded:
|
initialize_simps_projections
now by default generates all projections of all parent structures, and doesn't generate the projections to those parent structures.TwoPointed
)Internal changes:
ParsedProjectionData
to avoid the bug reported here (and to another bug where it seemed that the wrong data was inserted inParsedProjectionData
, but it was hard to minimize because of all the crashes). If we manage to fix the bug in that Zulip thread, I'll see if I can track down the other bug in commit 9745428This likely conflicts with future PRs, so please delegate instead of merge