[Merged by Bors] - feat: add a positivity extension for Real.toNNReal#31956
[Merged by Bors] - feat: add a positivity extension for Real.toNNReal#31956urkud wants to merge 7 commits intoleanprover-community:masterfrom
positivity extension for Real.toNNReal#31956Conversation
PR summary 567fa05a2eImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks!
maintainer delegate
| example (a : ℝ) : 0 ≤ a.nnabs := by positivity | ||
| example (a : ℝ) (ha : 0 < a) : 0 < a.nnabs := by positivity | ||
| example (a : ℝ) (ha : a ≠ 0) : 0 < a.nnabs := by positivity | ||
| example (a : ℝ≥0) (ha : 0 < a) : 0 < (a : ℝ) := by positivity |
There was a problem hiding this comment.
Similarly,
| example (a : ℝ≥0) (ha : 0 < a) : 0 < (a : ℝ) := by positivity | |
| example (a : ℝ≥0) (ha : a ≠ 0) : 0 < (a : ℝ) := by positivity |
There was a problem hiding this comment.
Sorry, I meant to add a new test, not replace the existing one!
There was a problem hiding this comment.
We know that positivity transforms a ≠ 0 into 0 < a for NNReals anyway.
There was a problem hiding this comment.
I know, but that's not a guarantee that adding this extra example will not uncover a bug
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
bors d+ |
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Yaël Yanis Dillies <yael.dillies@gmail.com>
|
As this PR is labelled bors merge |
|
Pull request successfully merged into master. Build succeeded: |
positivity extension for Real.toNNRealpositivity extension for Real.toNNReal
Uh oh!
There was an error while loading. Please reload this page.