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] - chore: remove unneeded decreasing_by and termination_by #11386
Conversation
LGTM. Thanks! There is an overlap with #11388 which is currently on the queue. AFAICT, the overlap won't generate merge conflicts. bors merge |
The termination checker has been getting more capable, and many of the `termination_by` or `decreasing_by` clauses in Mathlib are no longer needed. (Note that `termination_by?` will show the automatically derived termination expression, so no information is being lost by removing these.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
!bench Note that there is a performance penalty if you don't specify the measure, so I don't know if I actually recommend removing these annotations if you already have them. |
Pull request successfully merged into master. Build succeeded: |
Here are the benchmark results for commit 0a38691. |
Ok, the speedcenter alleviates my worries. Thanks! |
The termination checker has been getting more capable, and many of the `termination_by` or `decreasing_by` clauses in Mathlib are no longer needed. (Note that `termination_by?` will show the automatically derived termination expression, so no information is being lost by removing these.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
The termination checker has been getting more capable, and many of the `termination_by` or `decreasing_by` clauses in Mathlib are no longer needed. (Note that `termination_by?` will show the automatically derived termination expression, so no information is being lost by removing these.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
The termination checker has been getting more capable, and many of the `termination_by` or `decreasing_by` clauses in Mathlib are no longer needed. (Note that `termination_by?` will show the automatically derived termination expression, so no information is being lost by removing these.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
The termination checker has been getting more capable, and many of the `termination_by` or `decreasing_by` clauses in Mathlib are no longer needed. (Note that `termination_by?` will show the automatically derived termination expression, so no information is being lost by removing these.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
The termination checker has been getting more capable, and many of the `termination_by` or `decreasing_by` clauses in Mathlib are no longer needed. (Note that `termination_by?` will show the automatically derived termination expression, so no information is being lost by removing these.) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
The termination checker has been getting more capable, and many of the
termination_by
ordecreasing_by
clauses in Mathlib are no longer needed.(Note that
termination_by?
will show the automatically derived termination expression, so no information is being lost by removing these.)Pinging @nomeata as they might be pleased to see what is now possible!