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(tactic/simps): implement prefix names #7596
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me, thanks! I'm not an experienced simps
user, so I'll ask someone else to review it as well.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks great, thanks!
bors merge |
* You can now write `initialize_simps_projections equiv (to_fun → coe as_prefix)` to add the projection name as a prefix to the simp lemmas: if you then write `@[simps coe] def foo ...` you get a lemma named `coe_foo`. * Remove the `short_name` option from `simps_cfg`. This was unused and not that useful. * Refactor some tuples used in the functions into structures. * Implements one item of #5489.
Pull request successfully merged into master. Build succeeded: |
initialize_simps_projections equiv (to_fun → coe as_prefix)
to add the projection name as a prefix to the simp lemmas: if you then write@[simps coe] def foo ...
you get a lemma namedcoe_foo
.short_name
option fromsimps_cfg
. This was unused and not that useful.Requested by @b-mehta and @eric-wieser