diff options
| author | Kazuhiko Sakaguchi | 2020-10-31 14:20:16 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-11-13 21:07:20 +0900 |
| commit | 2f906481423530b03f21ff605aaee3f281131608 (patch) | |
| tree | 212ba9aa5bd6290afcc38b0ac908376ab8f78a92 /CHANGELOG_UNRELEASED.md | |
| parent | 2cc9e05d1fc4e6afb2dbb96e6cba2cd0af0a009f (diff) | |
Rename `eq_sorted` lemmas to `sorted_eq` and generalize `sort_le_id`
- Rename `eq_sorted` lemmas to `sorted_eq` to address a naming inconsistency.
- Lemma `sort_le_id` has been generalized from `orderType` to `porderType`.
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d7c3306..436b0bc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -356,6 +356,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, generalized lemmas `sub_path_in`, `sub_sorted_in`, and `eq_path_in` for non-`eqType`s. +- in `order.v`, generalized `sort_le_id` for any `porderType`. + ### Renamed - `big_rmcond` -> `big_rmcond_in` (cf Changed section) @@ -403,6 +405,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). (`allpairs_consr` and `allpairs_catr` are now deprecated alias, and will be attributed to the new `perm_allpairs_catr`). +- in `path.v`, `eq_sorted(_irr)` -> `(irr_)sorted_eq` + - in `div.v` + `coprime_mul(l|r)` -> `coprimeM(l|r)` + `coprime_exp(l|r)` -> `coprimeX(l|r)` @@ -417,6 +421,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + `primes_(mul|exp)` -> `primes(M|X)` + `pnat_(mul|exp)` -> `pnat(M|X)` +- in `order.v`, `eq_sorted_(le|lt)` -> `(le|lt)_sorted_eq` + - in `ssralg.v` + `prodrMn` has been renamed `prodrMn_const` (with deprecation alias, cf. Added section) |