affeldt-aist
affeldt-aist
During the conversation about PR #869 , it was observed by @thery and others that custom entries might provide a way to generalize the `leRHS`, etc. patterns: ``` Declare Custom...
I am relaying a discussion from gitter. There is the old question of using omega (lia now) with ssrnat. One obvious solution is a bit of Ltac to switch from...
This issue is to record a suggestion to work on a PR made by @ggonthier about the PR #221 proposed by @hivert (merged in MathComp 1.11). On 2018-12-10: This contribution...
https://github.com/math-comp/analysis/blob/9ac498c5f38d1e4870ad4968bdd04d3e098de348/theories/sequences.v#L1635 to `nneseries_ge0`?
https://github.com/math-comp/analysis/blob/593c2448923f9b1577fbc97a871f75a8b43ac233/theories/measure.v#L866 shouldn't be this better named `discrete_measurable_nat` or `measurable_nat`?
https://github.com/math-comp/analysis/blob/fe3e6730467a67a155e1873800565bd87a5d17e7/theories/measure.v#L1971-L1976 Since this definition does not use `fset` anymore, it should maybe be renamed. Maybe `ring_finite_set`?
https://github.com/math-comp/analysis/blob/9ac498c5f38d1e4870ad4968bdd04d3e098de348/theories/constructive_ereal.v#L492-L496 rename to `fine_ge0` and `fine_gt0`?
##### Motivation for this change ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~- [ ] added corresponding documentation in the headers~ ##### Automatic note to reviewers...
https://github.com/math-comp/analysis/blob/82e29a05dfc54f40bf576961bec7fdd6bdfb5c34/theories/measure.v#L2278-L2282 maybe it'd better be `cvg_measure_inc` to avoid using the name of the variable `mu`
##### Motivation for this change fixes #664 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` ~~- [ ] added corresponding documentation in the headers~~ ##### Automatic note...